[sledge] Improve backtraces of invariant violation and replay exceptions

Reviewed By: ngorogiannis

Differential Revision: D24630526

fbshipit-source-id: 0f879e84e

sledge/cli/sledge_cli.ml

@@ -51,14 +51,9 @@ let command ~summary ?readme param =
   let report main () =
     try main () |> Report.status
     with exn ->
-      let bt =
+      let bt = Printexc.get_raw_backtrace () in
-        match exn with
-        | Invariant.Violation (_, bt, _, _) -> bt
-        | Replay (_, bt, _) -> bt
-        | _ -> Printexc.get_raw_backtrace ()
-      in
       let rec status_of_exn = function
-        | Invariant.Violation (exn, _, _, _) | Replay (exn, _, _) ->
+        | Invariant.Violation (exn, _, _) | Replay (exn, _) ->
             status_of_exn exn
         | Frontend.Invalid_llvm msg -> Report.InvalidInput msg
         | Unimplemented msg -> Report.Unimplemented msg

sledge/nonstdlib/NS.mli

@@ -178,8 +178,7 @@ end
 
 (** Invariants *)
 module Invariant : sig
-  exception
+  exception Violation of exn * Lexing.position * Sexp.t
-    Violation of exn * Printexc.raw_backtrace * Lexing.position * Sexp.t
 
   val invariant :
     Lexing.position -> 'a -> ('a -> Sexp.t) -> (unit -> unit) -> unit
@@ -193,7 +192,7 @@ end
 
 (** Failures *)
 
-exception Replay of exn * Printexc.raw_backtrace * Sexp.t
+exception Replay of exn * Sexp.t
 exception Unimplemented of string
 
 val fail : ('a, unit -> _) fmt -> 'a

sledge/nonstdlib/NS0.ml

@@ -148,14 +148,13 @@ module Invariant = struct
     {pos_fname: string; pos_lnum: int; pos_bol: int; pos_cnum: int}
   [@@deriving sexp_of]
 
-  exception Violation of exn * Printexc.raw_backtrace * position * Sexp.t
+  exception Violation of exn * position * Sexp.t
 
   ;;
   register_sexp_of_exn
-    (Violation
+    (Violation (Not_found, Lexing.dummy_pos, Sexp.List []))
-       (Not_found, Printexc.get_callstack 1, Lexing.dummy_pos, Sexp.List []))
     (function
-      | Violation (exn, _, pos, payload) ->
+      | Violation (exn, pos, payload) ->
           Sexp.List
             [ Atom "Invariant.Violation"
             ; sexp_of_exn exn
@@ -168,7 +167,7 @@ module Invariant = struct
       ( try f ()
         with exn ->
           let bt = Printexc.get_raw_backtrace () in
-          let exn = Violation (exn, bt, here, sexp_of_t t) in
+          let exn = Violation (exn, here, sexp_of_t t) in
           Printexc.raise_with_backtrace exn bt ) ;
       true )
 
@@ -181,13 +180,13 @@ end
 
 (** Failures *)
 
-exception Replay of exn * Printexc.raw_backtrace * Sexp.t
+exception Replay of exn * Sexp.t
 
 ;;
 register_sexp_of_exn
-  (Replay (Not_found, Printexc.get_callstack 1, Sexp.List []))
+  (Replay (Not_found, Sexp.List []))
   (function
-    | Replay (exn, _, payload) ->
+    | Replay (exn, payload) ->
         Sexp.List [Atom "Replay"; sexp_of_exn exn; payload]
     | exn -> Sexp.Atom (Printexc.to_string exn) )
 

sledge/ppx_trace/trace/trace.ml

@@ -224,7 +224,6 @@ let trace :
         Printexc.raise_with_backtrace exc bt )
 
 let raisef ?margin exn fmt =
-  let bt = Printexc.get_raw_backtrace () in
   let fs = Format.str_formatter in
   ( match margin with
   | Some m ->
@@ -235,9 +234,7 @@ let raisef ?margin exn fmt =
   Format.kfprintf
     (fun fs () ->
       Format.pp_close_box fs () ;
-      let msg = Format.flush_str_formatter () in
+      raise (exn (Format.flush_str_formatter ())) )
-      let exn = exn msg in
-      Printexc.raise_with_backtrace exn bt )
     fs fmt
 
 let fail fmt =

sledge/src/fol/context.ml

@@ -1142,8 +1142,8 @@ let wrap tmr f call =
     try f ()
     with exn ->
       let bt = Printexc.get_raw_backtrace () in
-      let sexp = sexp_of_call (call ()) in
+      let exn = Replay (exn, sexp_of_call (call ())) in
-      raise (Replay (exn, bt, sexp))
+      Printexc.raise_with_backtrace exn bt
 
 let add_tmr = Timer.create "add" ~at_exit:report
 let union_tmr = Timer.create "union" ~at_exit:report

sledge/src/sh.ml

@@ -284,8 +284,9 @@ let rec invariant q =
             assert (Var.Set.subset sjn.us ~of_:(Var.Set.union us xs)) ;
             invariant sjn ) )
   with exc ->
+    let bt = Printexc.get_raw_backtrace () in
     [%Trace.info "%a" pp q] ;
-    raise exc
+    Printexc.raise_with_backtrace exc bt
 
 (** Quantification and Vocabulary *)