diff --git a/sledge/.gitignore b/sledge/.gitignore
index e1471f11f..5e35f4ea6 100644
--- a/sledge/.gitignore
+++ b/sledge/.gitignore
@@ -1,15 +1,11 @@
 .llvm_build
 .llvm_install
 .merlin
+/bin/dune
+/lib/dune
+/lib/import/dune
 /llvm/
 /model/dune
-/src/config/dune
-/src/domain/dune
-/src/dune
-/src/import/dune
-/src/llair/dune
-/src/symbheap/dune
-/src/trace/dune
 /test/*/*.bc
 /test/*/*.bc.err
 /test/*/*.bc.out
diff --git a/sledge/Makefile b/sledge/Makefile
index 0786731c1..a51ff4493 100644
--- a/sledge/Makefile
+++ b/sledge/Makefile
@@ -6,9 +6,9 @@
 .PHONY: default
 default: exes
 
-EXES = src/sledge
+EXES = bin/sledge
 INSTALLS = sledge
-FMTS = @_build/dbg/src/fmt
+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
 
@@ -23,7 +23,7 @@ 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)
+DUNEINS = $(shell find lib bin model -name dune.in)
 DUNES = $(patsubst %.in,%,$(DUNEINS))
 
 .PHONY: dunes
diff --git a/sledge/src/config/config.ml b/sledge/bin/config.ml
similarity index 100%
rename from sledge/src/config/config.ml
rename to sledge/bin/config.ml
diff --git a/sledge/src/config/config.mli b/sledge/bin/config.mli
similarity index 100%
rename from sledge/src/config/config.mli
rename to sledge/bin/config.mli
diff --git a/sledge/src/dune.in b/sledge/bin/dune.in
similarity index 60%
rename from sledge/src/dune.in
rename to sledge/bin/dune.in
index ca8117944..376e16d3b 100644
--- a/sledge/src/dune.in
+++ b/sledge/bin/dune.in
@@ -6,7 +6,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-let deps = ["import"; "trace"; "llair_"; "symbheap"; "config"; "domain"]
+let deps = ["import"; "libsledge"; "model"]
 
 ;;
 Jbuild_plugin.V1.send
@@ -15,8 +15,8 @@ Jbuild_plugin.V1.send
 (executable
  (public_name sledge)
  (package sledge)
- %s
- (libraries dune-build-info shexp.process %s))
+ (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)
-     (libraries deps)
diff --git a/sledge/src/llair/frontend.ml b/sledge/bin/frontend.ml
similarity index 100%
rename from sledge/src/llair/frontend.ml
rename to sledge/bin/frontend.ml
diff --git a/sledge/src/llair/frontend.mli b/sledge/bin/frontend.mli
similarity index 100%
rename from sledge/src/llair/frontend.mli
rename to sledge/bin/frontend.mli
diff --git a/sledge/src/sledge.ml b/sledge/bin/sledge.ml
similarity index 95%
rename from sledge/src/sledge.ml
rename to sledge/bin/sledge.ml
index 89bb3c24e..b652bceaa 100644
--- a/sledge/src/sledge.ml
+++ b/sledge/bin/sledge.ml
@@ -13,10 +13,10 @@ open Command.Let_syntax
 
 type 'a param = 'a Command.Param.t
 
-module Sh_executor = Control.Make (Domain.Relation.Make (Sh_domain))
-module Unit_executor = Control.Make (Domain.Unit)
-module Used_globals_executor = Control.Make (Domain.Used_globals)
-module Itv_executor = Control.Make (Domain.Itv)
+module Sh_executor = Control.Make (Domain_relation.Make (Domain_sh))
+module Unit_executor = Control.Make (Domain_unit)
+module Used_globals_executor = Control.Make (Domain_used_globals)
+module Itv_executor = Control.Make (Domain_itv)
 
 (* reverse application in the Command.Param applicative *)
 let ( |*> ) : 'a param -> ('a -> 'b) param -> 'b param =
@@ -70,7 +70,7 @@ let unmarshal file () =
     ~f:(fun ic -> (Marshal.from_channel ic : Llair.t))
     file
 
-let used_globals pgm preanalyze : Used_globals.r =
+let used_globals pgm preanalyze : Domain_used_globals.r =
   if preanalyze then
     let summary_table =
       Used_globals_executor.compute_summaries
@@ -122,7 +122,7 @@ let analyze =
     let globals = used_globals pgm preanalyze_globals in
     let entry_points = Config.find_list "entry-points" in
     let skip_throw = not exceptions in
-    Sh_domain.simplify_states := not no_simplify_states ;
+    Domain_sh.simplify_states := not no_simplify_states ;
     exec {bound; skip_throw; function_summaries; entry_points; globals} pgm
 
 let analyze_cmd =
diff --git a/sledge/src/sledge.mli b/sledge/bin/sledge.mli
similarity index 100%
rename from sledge/src/sledge.mli
rename to sledge/bin/sledge.mli
diff --git a/sledge/src/sledge_buck.ml b/sledge/bin/sledge_buck.ml
similarity index 100%
rename from sledge/src/sledge_buck.ml
rename to sledge/bin/sledge_buck.ml
diff --git a/sledge/src/sledge_buck.mli b/sledge/bin/sledge_buck.mli
similarity index 100%
rename from sledge/src/sledge_buck.mli
rename to sledge/bin/sledge_buck.mli
diff --git a/sledge/src/version.ml b/sledge/bin/version.ml
similarity index 100%
rename from sledge/src/version.ml
rename to sledge/bin/version.ml
diff --git a/sledge/src/version.mli b/sledge/bin/version.mli
similarity index 100%
rename from sledge/src/version.mli
rename to sledge/bin/version.mli
diff --git a/sledge/dune b/sledge/dune
index 3ed3699a8..6535e144c 100644
--- a/sledge/dune
+++ b/sledge/dune
@@ -1,8 +1,13 @@
+; 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.
+
 (ignored_subdirs (llvm test))
 
 (rule
  (targets sledge-help.txt)
- (deps src/sledge.ml src/sledge_buck.ml tools/gen_help.sh src/sledge.exe)
+ (deps bin/sledge.ml bin/sledge_buck.ml tools/gen_help.sh bin/sledge.exe)
  (action
   (with-stdout-to sledge-help.txt
    (run tools/gen_help.sh)))
diff --git a/sledge/src/control.ml b/sledge/lib/control.ml
similarity index 98%
rename from sledge/src/control.ml
rename to sledge/lib/control.ml
index 0b74854fa..32ffb4c43 100644
--- a/sledge/src/control.ml
+++ b/sledge/lib/control.ml
@@ -14,9 +14,9 @@ type exec_opts =
   ; skip_throw: bool
   ; function_summaries: bool
   ; entry_points: string list
-  ; globals: Used_globals.r }
+  ; globals: Domain_used_globals.r }
 
-module Make (Dom : Domain_sig.Dom) = struct
+module Make (Dom : Domain_intf.Dom) = struct
   module Stack : sig
     type t
     type as_inlined_location = t [@@deriving compare, sexp_of]
@@ -313,7 +313,9 @@ module Make (Dom : Domain_sig.Dom) = struct
     let summarize post_state =
       if not opts.function_summaries then post_state
       else
-        let globals = Used_globals.by_function opts.globals name.reg in
+        let globals =
+          Domain_used_globals.by_function opts.globals name.reg
+        in
         let function_summary, post_state =
           Dom.create_summary ~locals post_state
             ~formals:(Set.union (Reg.Set.of_list formals) globals)
@@ -435,7 +437,7 @@ module Make (Dom : Domain_sig.Dom) = struct
                     exec_skip_func stk state block areturn return
                 | None ->
                     exec_call opts stk state block {call with callee}
-                      (Used_globals.by_function opts.globals
+                      (Domain_used_globals.by_function opts.globals
                          callee.name.reg) )
                 |> Work.seq x ) )
     | Return {exp} -> exec_return ~opts stk state block exp
@@ -470,7 +472,8 @@ module Make (Dom : Domain_sig.Dom) = struct
           (Work.init
              (fst
                 (Dom.call ~summaries:opts.function_summaries
-                   ~globals:(Used_globals.by_function opts.globals reg)
+                   ~globals:
+                     (Domain_used_globals.by_function opts.globals reg)
                    ~actuals:[] ~areturn:None ~formals:[] ~freturn ~locals
                    (Dom.init pgm.globals)))
              entry)
diff --git a/sledge/src/control.mli b/sledge/lib/control.mli
similarity index 88%
rename from sledge/src/control.mli
rename to sledge/lib/control.mli
index 3faddab04..2c1feb9d9 100644
--- a/sledge/src/control.mli
+++ b/sledge/lib/control.mli
@@ -12,9 +12,9 @@ type exec_opts =
   ; skip_throw: bool  (** Treat throw as unreachable *)
   ; function_summaries: bool  (** Use function summarisation *)
   ; entry_points: string list
-  ; globals: Used_globals.r }
+  ; globals: Domain_used_globals.r }
 
-module Make (Dom : Domain_sig.Dom) : sig
+module Make (Dom : Domain_intf.Dom) : sig
   val exec_pgm : exec_opts -> Llair.t -> unit
   val compute_summaries : exec_opts -> Llair.t -> Dom.summary list Reg.Map.t
 end
diff --git a/sledge/src/domain/domain_sig.ml b/sledge/lib/domain_intf.ml
similarity index 100%
rename from sledge/src/domain/domain_sig.ml
rename to sledge/lib/domain_intf.ml
diff --git a/sledge/src/domain/itv.ml b/sledge/lib/domain_itv.ml
similarity index 100%
rename from sledge/src/domain/itv.ml
rename to sledge/lib/domain_itv.ml
diff --git a/sledge/src/domain/itv.mli b/sledge/lib/domain_itv.mli
similarity index 90%
rename from sledge/src/domain/itv.mli
rename to sledge/lib/domain_itv.mli
index 7f6309ae3..19ab2c841 100644
--- a/sledge/src/domain/itv.mli
+++ b/sledge/lib/domain_itv.mli
@@ -7,4 +7,4 @@
 
 (** Interval abstract domain *)
 
-include Domain_sig.Dom
+include Domain_intf.Dom
diff --git a/sledge/src/domain/relation.ml b/sledge/lib/domain_relation.ml
similarity index 99%
rename from sledge/src/domain/relation.ml
rename to sledge/lib/domain_relation.ml
index 957a72080..8e11a20c3 100644
--- a/sledge/src/domain/relation.ml
+++ b/sledge/lib/domain_relation.ml
@@ -9,7 +9,7 @@
     triples over a base state domain *)
 
 module type State_domain_sig = sig
-  include Domain_sig.Dom
+  include Domain_intf.Dom
 
   val create_summary :
        locals:Reg.Set.t
diff --git a/sledge/src/domain/relation.mli b/sledge/lib/domain_relation.mli
similarity index 83%
rename from sledge/src/domain/relation.mli
rename to sledge/lib/domain_relation.mli
index 6ef12d598..b14109532 100644
--- a/sledge/src/domain/relation.mli
+++ b/sledge/lib/domain_relation.mli
@@ -9,7 +9,7 @@
     triples over a base domain *)
 
 module type State_domain_sig = sig
-  include Domain_sig.Dom
+  include Domain_intf.Dom
 
   val create_summary :
        locals:Reg.Set.t
@@ -19,4 +19,4 @@ module type State_domain_sig = sig
     -> summary * t
 end
 
-module Make (State_domain : State_domain_sig) : Domain_sig.Dom
+module Make (State_domain : State_domain_sig) : Domain_intf.Dom
diff --git a/sledge/src/symbheap/sh_domain.ml b/sledge/lib/domain_sh.ml
similarity index 100%
rename from sledge/src/symbheap/sh_domain.ml
rename to sledge/lib/domain_sh.ml
diff --git a/sledge/src/symbheap/sh_domain.mli b/sledge/lib/domain_sh.mli
similarity index 95%
rename from sledge/src/symbheap/sh_domain.mli
rename to sledge/lib/domain_sh.mli
index a7912d12e..362d8257e 100644
--- a/sledge/src/symbheap/sh_domain.mli
+++ b/sledge/lib/domain_sh.mli
@@ -7,7 +7,7 @@
 
 (** Abstract domain *)
 
-include Domain_sig.Dom
+include Domain_intf.Dom
 
 (* formals should include all the parameters of the summary. That is both
    formals and globals. *)
diff --git a/sledge/src/domain/unit.ml b/sledge/lib/domain_unit.ml
similarity index 100%
rename from sledge/src/domain/unit.ml
rename to sledge/lib/domain_unit.ml
diff --git a/sledge/src/domain/unit.mli b/sledge/lib/domain_unit.mli
similarity index 90%
rename from sledge/src/domain/unit.mli
rename to sledge/lib/domain_unit.mli
index 93f619c01..f188c2fbd 100644
--- a/sledge/src/domain/unit.mli
+++ b/sledge/lib/domain_unit.mli
@@ -7,4 +7,4 @@
 
 (** "Unit" abstract domain *)
 
-include Domain_sig.Dom
+include Domain_intf.Dom
diff --git a/sledge/src/domain/used_globals.ml b/sledge/lib/domain_used_globals.ml
similarity index 100%
rename from sledge/src/domain/used_globals.ml
rename to sledge/lib/domain_used_globals.ml
diff --git a/sledge/src/domain/used_globals.mli b/sledge/lib/domain_used_globals.mli
similarity index 88%
rename from sledge/src/domain/used_globals.mli
rename to sledge/lib/domain_used_globals.mli
index 9cc13dd27..81bdc3b21 100644
--- a/sledge/src/domain/used_globals.mli
+++ b/sledge/lib/domain_used_globals.mli
@@ -7,7 +7,7 @@
 
 (** Used-globals abstract domain *)
 
-include Domain_sig.Dom with type summary = Reg.Set.t
+include Domain_intf.Dom with type summary = Reg.Set.t
 
 type r =
   | Per_function of Reg.Set.t Reg.Map.t
diff --git a/sledge/src/trace/dune.in b/sledge/lib/dune.in
similarity index 73%
rename from sledge/src/trace/dune.in
rename to sledge/lib/dune.in
index 180a95f89..e9c1b8fcd 100644
--- a/sledge/src/trace/dune.in
+++ b/sledge/lib/dune.in
@@ -13,10 +13,9 @@ Jbuild_plugin.V1.send
 @@ Format.sprintf
      {|
 (library
- (name trace)
- (public_name llair.trace)
- %s
- (libraries %s))
+ (name libsledge)
+ (libraries apron apron.boxMPQ ctypes ctypes.foreign %s)
+ %s)
 |}
+     (libraries ("trace" :: deps))
      (flags `lib deps)
-     (libraries deps)
diff --git a/sledge/src/symbheap/equality.ml b/sledge/lib/equality.ml
similarity index 100%
rename from sledge/src/symbheap/equality.ml
rename to sledge/lib/equality.ml
diff --git a/sledge/src/symbheap/equality.mli b/sledge/lib/equality.mli
similarity index 100%
rename from sledge/src/symbheap/equality.mli
rename to sledge/lib/equality.mli
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/lib/equality_test.ml
similarity index 100%
rename from sledge/src/symbheap/equality_test.ml
rename to sledge/lib/equality_test.ml
diff --git a/sledge/src/symbheap/equality_test.mli b/sledge/lib/equality_test.mli
similarity index 100%
rename from sledge/src/symbheap/equality_test.mli
rename to sledge/lib/equality_test.mli
diff --git a/sledge/src/symbheap/exec.ml b/sledge/lib/exec.ml
similarity index 100%
rename from sledge/src/symbheap/exec.ml
rename to sledge/lib/exec.ml
diff --git a/sledge/src/symbheap/exec.mli b/sledge/lib/exec.mli
similarity index 100%
rename from sledge/src/symbheap/exec.mli
rename to sledge/lib/exec.mli
diff --git a/sledge/src/llair/exp.ml b/sledge/lib/exp.ml
similarity index 100%
rename from sledge/src/llair/exp.ml
rename to sledge/lib/exp.ml
diff --git a/sledge/src/llair/exp.mli b/sledge/lib/exp.mli
similarity index 100%
rename from sledge/src/llair/exp.mli
rename to sledge/lib/exp.mli
diff --git a/sledge/src/llair/exp_test.ml b/sledge/lib/exp_test.ml
similarity index 92%
rename from sledge/src/llair/exp_test.ml
rename to sledge/lib/exp_test.ml
index 07bb74028..cebaece49 100644
--- a/sledge/src/llair/exp_test.ml
+++ b/sledge/lib/exp_test.ml
@@ -7,8 +7,8 @@
 
 let%test_module _ =
   ( module struct
-    (* let () = Trace.init ~margin:68 ~config:all () *)
-    let () = Trace.init ~margin:68 ~config:none ()
+    (* let () = Trace.init ~margin:68 ~config:Trace.all () *)
+    let () = Trace.init ~margin:68 ()
 
     open Exp
 
diff --git a/sledge/src/llair/exp_test.mli b/sledge/lib/exp_test.mli
similarity index 100%
rename from sledge/src/llair/exp_test.mli
rename to sledge/lib/exp_test.mli
diff --git a/sledge/src/llair/global.ml b/sledge/lib/global.ml
similarity index 100%
rename from sledge/src/llair/global.ml
rename to sledge/lib/global.ml
diff --git a/sledge/src/llair/global.mli b/sledge/lib/global.mli
similarity index 100%
rename from sledge/src/llair/global.mli
rename to sledge/lib/global.mli
diff --git a/sledge/src/import/dune.in b/sledge/lib/import/dune.in
similarity index 73%
rename from sledge/src/import/dune.in
rename to sledge/lib/import/dune.in
index 778cfdab8..258310500 100644
--- a/sledge/src/import/dune.in
+++ b/sledge/lib/import/dune.in
@@ -14,9 +14,9 @@ Jbuild_plugin.V1.send
      {|
 (library
  (name import)
- (public_name llair.import)
- %s
- (libraries core core_kernel.fheap zarith %s))
+ (public_name sledge.import)
+ (libraries core core_kernel.fheap zarith %s)
+ %s)
 |}
+     (libraries ("trace" :: deps))
      (flags `lib deps)
-     (libraries deps)
diff --git a/sledge/src/import/import.ml b/sledge/lib/import/import.ml
similarity index 93%
rename from sledge/src/import/import.ml
rename to sledge/lib/import/import.ml
index daa64eec5..c27f11c01 100644
--- a/sledge/src/import/import.ml
+++ b/sledge/lib/import/import.ml
@@ -48,10 +48,16 @@ let ( <$ ) f x = f x ; x
 (** Pretty-printing *)
 
 type 'a pp = Formatter.t -> 'a -> unit
-type ('a, 'b) fmt = ('a, Formatter.t, unit, 'b) format4
+type ('a, 'b) fmt = ('a, 'b) Trace.fmt
 
 (** Failures *)
 
+let fail = Trace.fail
+
+exception Unimplemented of string
+
+let todo fmt = Trace.raisef (fun msg -> Unimplemented msg) fmt
+
 let warn fmt =
   let fs = Format.std_formatter in
   Format.pp_open_box fs 2 ;
@@ -62,27 +68,7 @@ let warn fmt =
       Format.pp_force_newline fs () )
     fs fmt
 
-let raisef ?margin exn fmt =
-  let bt = Caml.Printexc.get_raw_backtrace () in
-  let fs = Format.str_formatter in
-  ( match margin with
-  | Some m ->
-      Format.pp_set_margin fs m ;
-      Format.pp_set_max_indent fs (m - 1)
-  | None -> () ) ;
-  Format.pp_open_box fs 2 ;
-  Format.kfprintf
-    (fun fs () ->
-      Format.pp_close_box fs () ;
-      let msg = Format.flush_str_formatter () in
-      let exn = exn msg in
-      Caml.Printexc.raise_with_backtrace exn bt )
-    fs fmt
-
-exception Unimplemented of string
-
-let todo fmt = raisef (fun msg -> Unimplemented msg) fmt
-let fail fmt = raisef (fun msg -> Failure msg) fmt
+(** Assertions *)
 
 let assertf cnd fmt =
   if not cnd then fail fmt
diff --git a/sledge/src/import/import.mli b/sledge/lib/import/import.mli
similarity index 95%
rename from sledge/src/import/import.mli
rename to sledge/lib/import/import.mli
index 467aed91d..05edbba6f 100644
--- a/sledge/src/import/import.mli
+++ b/sledge/lib/import/import.mli
@@ -69,24 +69,25 @@ val ( <$ ) : ('a -> unit) -> 'a -> 'a
 type 'a pp = Formatter.t -> 'a -> unit
 
 (** Format strings. *)
-type ('a, 'b) fmt = ('a, Formatter.t, unit, 'b) format4
+type ('a, 'b) fmt = ('a, 'b) Trace.fmt
 
 (** Failures *)
 
 exception Unimplemented of string
 
-val raisef : ?margin:int -> (string -> exn) -> ('a, unit -> _) fmt -> 'a
-(** Take a function from a string message to an exception, and a format
-    string with the additional arguments it specifies, and then call the
-    function on the formatted string and raise the returned exception. *)
-
-val warn : ('a, unit -> unit) fmt -> 'a
-(** Issue a warning for a survivable problem. *)
+val fail : ('a, unit -> _) fmt -> 'a
+(** Emit a message at the current indentation level, and raise a [Failure]
+    exception indicating a fatal error. *)
 
 val todo : ('a, unit -> _) fmt -> 'a
 (** Raise an [Unimplemented] exception indicating that an input is valid but
     not handled by the current implementation. *)
 
+val warn : ('a, unit -> unit) fmt -> 'a
+(** Issue a warning for a survivable problem. *)
+
+(** Assertions *)
+
 val assertf : bool -> ('a, unit -> unit) fmt -> 'a
 (** Raise an [Failure] exception if the bool argument is false, indicating
     that the expected condition was not satisfied. *)
diff --git a/sledge/src/import/qset.ml b/sledge/lib/import/qset.ml
similarity index 100%
rename from sledge/src/import/qset.ml
rename to sledge/lib/import/qset.ml
diff --git a/sledge/src/import/qset.mli b/sledge/lib/import/qset.mli
similarity index 100%
rename from sledge/src/import/qset.mli
rename to sledge/lib/import/qset.mli
diff --git a/sledge/src/import/vector.ml b/sledge/lib/import/vector.ml
similarity index 100%
rename from sledge/src/import/vector.ml
rename to sledge/lib/import/vector.ml
diff --git a/sledge/src/import/vector.mli b/sledge/lib/import/vector.mli
similarity index 100%
rename from sledge/src/import/vector.mli
rename to sledge/lib/import/vector.mli
diff --git a/sledge/src/llair/llair.ml b/sledge/lib/llair.ml
similarity index 100%
rename from sledge/src/llair/llair.ml
rename to sledge/lib/llair.ml
diff --git a/sledge/src/llair/llair.mli b/sledge/lib/llair.mli
similarity index 100%
rename from sledge/src/llair/llair.mli
rename to sledge/lib/llair.mli
diff --git a/sledge/src/llair/loc.ml b/sledge/lib/loc.ml
similarity index 100%
rename from sledge/src/llair/loc.ml
rename to sledge/lib/loc.ml
diff --git a/sledge/src/llair/loc.mli b/sledge/lib/loc.mli
similarity index 100%
rename from sledge/src/llair/loc.mli
rename to sledge/lib/loc.mli
diff --git a/sledge/src/llair/reg.ml b/sledge/lib/reg.ml
similarity index 100%
rename from sledge/src/llair/reg.ml
rename to sledge/lib/reg.ml
diff --git a/sledge/src/llair/reg.mli b/sledge/lib/reg.mli
similarity index 100%
rename from sledge/src/llair/reg.mli
rename to sledge/lib/reg.mli
diff --git a/sledge/src/report.ml b/sledge/lib/report.ml
similarity index 100%
rename from sledge/src/report.ml
rename to sledge/lib/report.ml
diff --git a/sledge/src/report.mli b/sledge/lib/report.mli
similarity index 100%
rename from sledge/src/report.mli
rename to sledge/lib/report.mli
diff --git a/sledge/src/symbheap/sh.ml b/sledge/lib/sh.ml
similarity index 100%
rename from sledge/src/symbheap/sh.ml
rename to sledge/lib/sh.ml
diff --git a/sledge/src/symbheap/sh.mli b/sledge/lib/sh.mli
similarity index 100%
rename from sledge/src/symbheap/sh.mli
rename to sledge/lib/sh.mli
diff --git a/sledge/src/symbheap/sh_test.ml b/sledge/lib/sh_test.ml
similarity index 100%
rename from sledge/src/symbheap/sh_test.ml
rename to sledge/lib/sh_test.ml
diff --git a/sledge/src/symbheap/sh_test.mli b/sledge/lib/sh_test.mli
similarity index 100%
rename from sledge/src/symbheap/sh_test.mli
rename to sledge/lib/sh_test.mli
diff --git a/sledge/src/symbheap/solver.ml b/sledge/lib/solver.ml
similarity index 99%
rename from sledge/src/symbheap/solver.ml
rename to sledge/lib/solver.ml
index 337f89290..c3d83d559 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/lib/solver.ml
@@ -136,8 +136,8 @@ let fresh_var name vs zs ~wrt =
   let v = Term.var v in
   (v, vs, zs, wrt)
 
-let excise k = [%Trace.infok k]
-let trace k = [%Trace.infok k]
+let excise (k : Trace.pf -> _) = [%Trace.infok k]
+let trace (k : Trace.pf -> _) = [%Trace.infok k]
 
 let excise_exists goal =
   trace (fun {pf} -> pf "@[<2>excise_exists@ %a@]" pp goal) ;
diff --git a/sledge/src/symbheap/solver.mli b/sledge/lib/solver.mli
similarity index 100%
rename from sledge/src/symbheap/solver.mli
rename to sledge/lib/solver.mli
diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/lib/solver_test.ml
similarity index 100%
rename from sledge/src/symbheap/solver_test.ml
rename to sledge/lib/solver_test.ml
diff --git a/sledge/src/symbheap/solver_test.mli b/sledge/lib/solver_test.mli
similarity index 100%
rename from sledge/src/symbheap/solver_test.mli
rename to sledge/lib/solver_test.mli
diff --git a/sledge/src/stop.ml b/sledge/lib/stop.ml
similarity index 100%
rename from sledge/src/stop.ml
rename to sledge/lib/stop.ml
diff --git a/sledge/src/stop.mli b/sledge/lib/stop.mli
similarity index 100%
rename from sledge/src/stop.mli
rename to sledge/lib/stop.mli
diff --git a/sledge/src/llair/term.ml b/sledge/lib/term.ml
similarity index 100%
rename from sledge/src/llair/term.ml
rename to sledge/lib/term.ml
diff --git a/sledge/src/llair/term.mli b/sledge/lib/term.mli
similarity index 100%
rename from sledge/src/llair/term.mli
rename to sledge/lib/term.mli
diff --git a/sledge/src/llair/term_test.ml b/sledge/lib/term_test.ml
similarity index 98%
rename from sledge/src/llair/term_test.ml
rename to sledge/lib/term_test.ml
index ad8de1264..f9bace39a 100644
--- a/sledge/src/llair/term_test.ml
+++ b/sledge/lib/term_test.ml
@@ -7,8 +7,8 @@
 
 let%test_module _ =
   ( module struct
-    (* let () = Trace.init ~margin:68 ~config:all () *)
-    let () = Trace.init ~margin:68 ~config:none ()
+    (* let () = Trace.init ~margin:68 ~config:Trace.all () *)
+    let () = Trace.init ~margin:68 ()
 
     open Term
 
diff --git a/sledge/src/llair/term_test.mli b/sledge/lib/term_test.mli
similarity index 100%
rename from sledge/src/llair/term_test.mli
rename to sledge/lib/term_test.mli
diff --git a/sledge/src/llair/typ.ml b/sledge/lib/typ.ml
similarity index 100%
rename from sledge/src/llair/typ.ml
rename to sledge/lib/typ.ml
diff --git a/sledge/src/llair/typ.mli b/sledge/lib/typ.mli
similarity index 100%
rename from sledge/src/llair/typ.mli
rename to sledge/lib/typ.mli
diff --git a/sledge/src/llair/var.ml b/sledge/lib/var.ml
similarity index 100%
rename from sledge/src/llair/var.ml
rename to sledge/lib/var.ml
diff --git a/sledge/src/llair/var.mli b/sledge/lib/var.mli
similarity index 100%
rename from sledge/src/llair/var.mli
rename to sledge/lib/var.mli
diff --git a/sledge/llair.opam b/sledge/llair.opam
deleted file mode 100644
index 2aa490923..000000000
--- a/sledge/llair.opam
+++ /dev/null
@@ -1,21 +0,0 @@
-opam-version: "1.2"
-maintainer: "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: [
-  [make "dunes"]
-  ["dune" "build" "-p" name "-j" jobs]
-]
-depends: [
-  "base" {>= "v0.12.0"}
-  "cmdliner"
-  "core_kernel" {>= "v0.11.0"}
-  "ctypes"
-  "ctypes-foreign"
-  "dune" {build}
-  "llvm" {build & = "7.0.0"}
-  "ppx_compare" {>= "v0.11.0"}
-  "ppx_hash" {>= "v0.11.0"}
-  "zarith"
-]
diff --git a/sledge/model/dune.in b/sledge/model/dune.in
index dadab2ee3..f33b39a28 100644
--- a/sledge/model/dune.in
+++ b/sledge/model/dune.in
@@ -22,7 +22,6 @@ Jbuild_plugin.V1.send
  (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)
@@ -30,9 +29,9 @@ Jbuild_plugin.V1.send
 
 (library
  (name model)
- (public_name llair.model)
- %s
- (libraries %s))
+ (public_name sledge.model)
+ (libraries %s)
+ %s)
 |}
-     (flags `lib deps)
      (libraries deps)
+     (flags `lib deps)
diff --git a/sledge/ppx_trace.opam b/sledge/ppx_trace.opam
new file mode 100644
index 000000000..ba5ce9bf0
--- /dev/null
+++ b/sledge/ppx_trace.opam
@@ -0,0 +1,18 @@
+opam-version: "2.0"
+maintainer: "Josh Berdine <jjb@fb.com>"
+authors: "Josh Berdine <jjb@fb.com>"
+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"
+  "base" {>= "v0.12.0"}
+  "dune" {>= "1.11.3" build}
+  "ppxlib"
+]
+synopsis: "Conditionally compiled debug tracing"
+description: "Conditionally compiled debug tracing"
diff --git a/sledge/src/ppx_trace/dune b/sledge/ppx_trace/dune
similarity index 100%
rename from sledge/src/ppx_trace/dune
rename to sledge/ppx_trace/dune
diff --git a/sledge/src/ppx_trace/ppx_trace.ml b/sledge/ppx_trace/ppx_trace.ml
similarity index 98%
rename from sledge/src/ppx_trace/ppx_trace.ml
rename to sledge/ppx_trace/ppx_trace.ml
index 411738550..295aad8fa 100644
--- a/sledge/src/ppx_trace/ppx_trace.ml
+++ b/sledge/ppx_trace/ppx_trace.ml
@@ -45,8 +45,7 @@ module Ast_mapper = Selected_ast.Ast.Ast_mapper
 let debug = ref false
 
 ;;
-Driver.add_arg "--debug" (Caml.Arg.Set debug)
-  ~doc:"Enable debug tracing output"
+Driver.add_arg "--debug" (Arg.Set debug) ~doc:"Enable debug tracing output"
 
 let rec get_fun_name pat =
   match pat.ppat_desc with
diff --git a/sledge/src/ppx_trace/ppx_trace.mli b/sledge/ppx_trace/ppx_trace.mli
similarity index 100%
rename from sledge/src/ppx_trace/ppx_trace.mli
rename to sledge/ppx_trace/ppx_trace.mli
diff --git a/sledge/ppx_trace/trace/dune b/sledge/ppx_trace/trace/dune
new file mode 100644
index 000000000..fafd9bdf2
--- /dev/null
+++ b/sledge/ppx_trace/trace/dune
@@ -0,0 +1,9 @@
+; 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)
+ (libraries base))
diff --git a/sledge/src/trace/trace.ml b/sledge/ppx_trace/trace/trace.ml
similarity index 86%
rename from sledge/src/trace/trace.ml
rename to sledge/ppx_trace/trace/trace.ml
index 4de7f6956..77ba22d5b 100644
--- a/sledge/src/trace/trace.ml
+++ b/sledge/ppx_trace/trace/trace.ml
@@ -5,9 +5,15 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+module Char = Base.Char
+module List = Base.List
+module Map = Base.Map
+module Option = Base.Option
+module String = Base.String
+
 (** Debug trace logging *)
 
-type 'a printf = ('a, Formatter.t, unit) format -> 'a
+type 'a printf = ('a, Format.formatter, unit) format -> 'a
 type pf = {pf: 'a. 'a printf}
 
 let fs = Format.err_formatter
@@ -98,7 +104,7 @@ let pp_styled style fmt fs =
         Format.pp_close_box fs () )
       fs fmt )
 
-let init ?(colors = false) ?(margin = 240) ~config:c () =
+let init ?(colors = false) ?(margin = 240) ?config:(c = none) () =
   Format.set_margin margin ;
   Format.set_max_indent (margin - 1) ;
   Format.pp_set_margin fs margin ;
@@ -119,7 +125,7 @@ let unwrap s =
   | None -> s
 
 let enabled mod_name fun_name =
-  let {trace_all; trace_mods_funs} = !config in
+  let {trace_all; trace_mods_funs; _} = !config in
   match Map.find trace_mods_funs (unwrap mod_name) with
   | Some {trace_mod; trace_funs} -> (
     match Map.find trace_funs fun_name with
@@ -168,6 +174,25 @@ let retn mod_name fun_name k result =
   k {pf= (fun fmt -> decf mod_name fun_name fmt)} result ;
   result
 
+type ('a, 'b) fmt = ('a, Base.Formatter.t, unit, 'b) format4
+
+let raisef ?margin exn fmt =
+  let bt = Caml.Printexc.get_raw_backtrace () in
+  let fs = Format.str_formatter in
+  ( match margin with
+  | Some m ->
+      Format.pp_set_margin fs m ;
+      Format.pp_set_max_indent fs (m - 1)
+  | None -> () ) ;
+  Format.pp_open_box fs 2 ;
+  Format.kfprintf
+    (fun fs () ->
+      Format.pp_close_box fs () ;
+      let msg = Format.flush_str_formatter () in
+      let exn = exn msg in
+      Caml.Printexc.raise_with_backtrace exn bt )
+    fs fmt
+
 let fail fmt =
   let margin = Format.pp_get_margin fs () in
   raisef ~margin
@@ -175,6 +200,3 @@ let fail fmt =
       Format.fprintf fs "@\n@[<2>| %s@]@." msg ;
       Failure msg )
     fmt
-
-let%test_module _ =
-  (module struct let () = init ~margin:70 ~config:!config () end)
diff --git a/sledge/src/trace/trace.mli b/sledge/ppx_trace/trace/trace.mli
similarity index 72%
rename from sledge/src/trace/trace.mli
rename to sledge/ppx_trace/trace/trace.mli
index c136bc2af..38cc2e19c 100644
--- a/sledge/src/trace/trace.mli
+++ b/sledge/ppx_trace/trace/trace.mli
@@ -11,10 +11,10 @@
 type trace_mod_funs =
   { trace_mod: bool option
         (** Enable/disable tracing of all functions in module *)
-  ; trace_funs: bool Map.M(String).t
+  ; trace_funs: bool Base.Map.M(Base.String).t
         (** Enable/disable tracing of individual functions *) }
 
-type trace_mods_funs = trace_mod_funs Map.M(String).t
+type trace_mods_funs = trace_mod_funs Base.Map.M(Base.String).t
 
 type config =
   { trace_all: bool  (** Enable all tracing *)
@@ -26,10 +26,10 @@ val none : config
 val all : config
 val parse : string -> (config, exn) result
 
-val init : ?colors:bool -> ?margin:int -> config:config -> unit -> unit
+val init : ?colors:bool -> ?margin:int -> ?config:config -> unit -> unit
 (** Initialize the configuration of debug tracing. *)
 
-type 'a printf = ('a, Formatter.t, unit) format -> 'a
+type 'a printf = ('a, Format.formatter, unit) format -> 'a
 type pf = {pf: 'a. 'a printf}
 
 val pp_styled :
@@ -42,10 +42,10 @@ val pp_styled :
 val printf : string -> string -> 'a printf
 (** Like [Format.printf], if enabled, otherwise like [Format.iprintf]. *)
 
-val fprintf : string -> string -> Formatter.t -> 'a printf
+val fprintf : string -> string -> Format.formatter -> 'a printf
 (** Like [Format.fprintf], if enabled, otherwise like [Format.ifprintf]. *)
 
-val kprintf : string -> string -> (Formatter.t -> unit) -> 'a printf
+val kprintf : string -> string -> (Format.formatter -> unit) -> 'a printf
 (** Like [Format.kprintf], if enabled, otherwise like [Format.ifprintf]. *)
 
 val info : string -> string -> 'a printf
@@ -63,6 +63,14 @@ val retn : string -> string -> (pf -> 'a -> unit) -> 'a -> 'a
 val flush : unit -> unit
 (** Flush the internal buffers. *)
 
+(** Format strings. *)
+type ('a, 'b) fmt = ('a, Format.formatter, unit, 'b) format4
+
+val raisef : ?margin:int -> (string -> exn) -> ('a, unit -> _) fmt -> 'a
+(** Take a function from a string message to an exception, and a format
+    string with the additional arguments it specifies, and then call the
+    function on the formatted string and raise the returned exception. *)
+
 val fail : ('a, unit -> _) fmt -> 'a
 (** Emit a message at the current indentation level, and raise a [Failure]
     exception indicating a fatal error. *)
diff --git a/sledge/src/config/dune.in b/sledge/src/config/dune.in
deleted file mode 100644
index f14f223b4..000000000
--- a/sledge/src/config/dune.in
+++ /dev/null
@@ -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"; "trace"]
-
-;;
-Jbuild_plugin.V1.send
-@@ Format.sprintf
-     {|
-(library
- (name config)
- (public_name llair.config)
- %s
- (libraries yojson %s))
-|}
-     (flags `lib deps)
-     (libraries deps)
diff --git a/sledge/src/domain/dune.in b/sledge/src/domain/dune.in
deleted file mode 100644
index ea37a6d50..000000000
--- a/sledge/src/domain/dune.in
+++ /dev/null
@@ -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"; "trace"; "llair_"]
-
-;;
-Jbuild_plugin.V1.send
-@@ Format.sprintf
-     {|
-(library
- (name domain)
- %s
- (libraries apron apron.boxMPQ %s))
-|}
-     (flags `lib deps)
-     (libraries deps)
diff --git a/sledge/src/llair/dune.in b/sledge/src/llair/dune.in
deleted file mode 100644
index e57cec4af..000000000
--- a/sledge/src/llair/dune.in
+++ /dev/null
@@ -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 = ["model"; "import"; "trace"; "config"]
-
-;;
-Jbuild_plugin.V1.send
-@@ Format.sprintf
-     {|
-(library
- (name llair_)
- (public_name llair)
- %s
- (libraries ctypes ctypes.foreign llvm llvm.irreader llvm.analysis llvm.scalar_opts llvm.target llvm.ipo llvm.linker %s))
-|}
-     (flags `lib deps)
-     (libraries deps)
diff --git a/sledge/src/symbheap/dune.in b/sledge/src/symbheap/dune.in
deleted file mode 100644
index c30fd12a2..000000000
--- a/sledge/src/symbheap/dune.in
+++ /dev/null
@@ -1,20 +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"; "trace"; "llair_"; "domain"]
-
-;;
-Jbuild_plugin.V1.send
-@@ Format.sprintf {|
-(library
- (name symbheap)
- %s
- (libraries %s))
-|}
-     (flags `lib deps)
-     (libraries deps)