From 52b511d0534fddedb179303f10efa7abf96d47a8 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 4 Nov 2020 02:08:36 -0800
Subject: [PATCH] [sledge] Improve backtraces of invariant violation and replay
 exceptions

Reviewed By: ngorogiannis

Differential Revision: D24630526

fbshipit-source-id: 0f879e84e
---
 sledge/cli/sledge_cli.ml        |  9 ++-------
 sledge/nonstdlib/NS.mli         |  5 ++---
 sledge/nonstdlib/NS0.ml         | 15 +++++++--------
 sledge/ppx_trace/trace/trace.ml |  5 +----
 sledge/src/fol/context.ml       |  4 ++--
 sledge/src/sh.ml                |  3 ++-
 6 files changed, 16 insertions(+), 25 deletions(-)

diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml
index 3575b2d74..4e2bfffb7 100644
--- a/sledge/cli/sledge_cli.ml
+++ b/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 =
-        match exn with
-        | Invariant.Violation (_, bt, _, _) -> bt
-        | Replay (_, bt, _) -> bt
-        | _ -> Printexc.get_raw_backtrace ()
-      in
+      let 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
diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli
index aec1d2473..c209ecf70 100644
--- a/sledge/nonstdlib/NS.mli
+++ b/sledge/nonstdlib/NS.mli
@@ -178,8 +178,7 @@ end
 
 (** Invariants *)
 module Invariant : sig
-  exception
-    Violation of exn * Printexc.raw_backtrace * Lexing.position * Sexp.t
+  exception Violation of exn * 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
diff --git a/sledge/nonstdlib/NS0.ml b/sledge/nonstdlib/NS0.ml
index d206531a9..507c42acd 100644
--- a/sledge/nonstdlib/NS0.ml
+++ b/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
-       (Not_found, Printexc.get_callstack 1, Lexing.dummy_pos, Sexp.List []))
+    (Violation (Not_found, 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) )
 
diff --git a/sledge/ppx_trace/trace/trace.ml b/sledge/ppx_trace/trace/trace.ml
index c138c49dd..f47ef0c34 100644
--- a/sledge/ppx_trace/trace/trace.ml
+++ b/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
-      let exn = exn msg in
-      Printexc.raise_with_backtrace exn bt )
+      raise (exn (Format.flush_str_formatter ())) )
     fs fmt
 
 let fail fmt =
diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 4b8131807..e08472c1a 100644
--- a/sledge/src/fol/context.ml
+++ b/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
-      raise (Replay (exn, bt, sexp))
+      let exn = Replay (exn, sexp_of_call (call ())) in
+      Printexc.raise_with_backtrace exn bt
 
 let add_tmr = Timer.create "add" ~at_exit:report
 let union_tmr = Timer.create "union" ~at_exit:report
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 340e01954..6543f5181 100644
--- a/sledge/src/sh.ml
+++ b/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 *)