[sledge] Add dbg-opt build mode

Summary:
This adds an optimized debug build mode, which is compiled with
optimizations, and without assertions, but still has tracing enabled.

Reviewed By: kren1

Differential Revision: D16069452

fbshipit-source-id: 445cfa329

sledge/Makefile

@@ -8,10 +8,11 @@ default: exes
 
 EXES = src/sledge
 INSTALLS = sledge
-FMTS = @_build/dev/src/fmt
+FMTS = @_build/dbg/src/fmt
 
-DBG_TARGETS = $(patsubst %,_build/dev/%.exe,$(EXES)) $(patsubst %,_build/dev/%.install,$(INSTALLS)) _build/dev/sledge-help.txt
-OPT_TARGETS = $(patsubst %,_build/release/%.exe,$(EXES)) $(patsubst %,_build/release/%.install,$(INSTALLS)) _build/release/sledge-help.txt
+DBG_TARGETS = $(patsubst %,_build/dbg/%.exe,$(EXES)) $(patsubst %,_build/dbg/%.install,$(INSTALLS)) _build/dbg/sledge-help.txt
+OPT_TARGETS = $(patsubst %,_build/opt/%.exe,$(EXES)) $(patsubst %,_build/opt/%.install,$(INSTALLS)) _build/opt/sledge-help.txt
+DBG_OPT_TARGETS = $(patsubst %,_build/dbg-opt/%.exe,$(EXES)) $(patsubst %,_build/dbg-opt/%.install,$(INSTALLS)) _build/dbg-opt/sledge-help.txt
 
 DUNEINS = $(shell find src model -name dune.in)
 DUNES = $(patsubst %.in,%,$(DUNEINS))
@@ -31,27 +32,31 @@ check: setup
 
 .PHONY: exes
 exes: setup
-	dune build $(DBG_TARGETS) $(OPT_TARGETS)
+	dune build $(DBG_TARGETS) $(DBG_OPT_TARGETS) $(OPT_TARGETS)
 
 .PHONY: dbg
 dbg: setup
 	dune build $(DBG_TARGETS)
 
+.PHONY: do
+do: setup
+	dune build $(DBG_OPT_TARGETS)
+
 .PHONY: opt
 opt: setup
 	dune build $(OPT_TARGETS)
 
 .PHONY: watch
 watch: setup
-	dune build --watch $(DBG_TARGETS) $(OPT_TARGETS)
+	dune build --watch $(DBG_TARGETS) $(DBG_OPT_TARGETS) $(OPT_TARGETS)
 
 .PHONY: test
 test: setup
-	dune build @_build/dev/runtest --auto-promote
+	dune build @_build/dbg/runtest --auto-promote
 
 .PHONY: ci-test
 ci-test: setup
-	dune build @_build/dev/runtest
+	dune build @_build/dbg/runtest
 
 BISECT_DIR = $(CURDIR)/_coverage/out
 

sledge/bin/sledge

@@ -1 +1 @@
-../_build/install/release/bin/sledge
+../_build/install/opt/bin/sledge

sledge/bin/sledge.dbg

@@ -1 +1 @@
-../_build/install/dev/bin/sledge
+../_build/install/dbg/bin/sledge

sledge/dune-common.in

@@ -14,19 +14,21 @@ let common_flags =
 
 let ocamlc_flags =
   match Jbuild_plugin.V1.context with
-  | "release" -> "-w -26-32 -noassert"
+  | "opt" | "dbg-opt" -> "-w -26-32 -noassert"
   | _ -> "-g"
 
 let ocamlopt_flags =
   match Jbuild_plugin.V1.context with
-  | "release" -> ocamlc_flags ^ " -w -a -O3"
+  | "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 "dev" -> "--debug" | _ -> ""
+  match Jbuild_plugin.V1.context with
+  | "dbg" | "dbg-opt" -> "--debug"
+  | _ -> ""
 
 let flags exe_or_lib deps =
   Printf.sprintf

sledge/dune-workspace

@@ -1,5 +1,6 @@
 (lang dune 1.0)
 
-(context (opam (switch sledge) (name dev) (merlin)))
+(context (opam (switch sledge) (name dbg) (merlin)))
+(context (opam (switch sledge) (name dbg-opt)))
+(context (opam (switch sledge) (name opt)))
 (context (opam (switch sledge) (name coverage)))
-(context (opam (switch sledge) (name release)))

sledge/sledge.opam

@@ -7,7 +7,7 @@ dev-repo: "git://github.com/facebook/infer.git"
 license: "MIT"
 build: [
   [make "setup"]
-  ["dune" "build" "-p" name "-j" jobs]
+  ["dune" "build" "-p" name "--profile" "opt" "-j" jobs]
 ]
 depends: [
   "ocaml"

sledge/src/import/import.ml

@@ -108,7 +108,8 @@ module Invariant = struct
   include Base.Invariant
 
   let invariant here t sexp_of_t f =
-    try f ()
+    assert (
+      ( try f ()
         with exn ->
           let bt = Caml.Printexc.get_raw_backtrace () in
           let exn =
@@ -119,7 +120,8 @@ module Invariant = struct
                     ; ("exn", sexp_of_exn exn)
                     ; ("", sexp_of_t t) ]))
           in
-      Caml.Printexc.raise_with_backtrace exn bt
+          Caml.Printexc.raise_with_backtrace exn bt ) ;
+      true )
 end
 
 let map_preserving_phys_equal map t ~f =