From 3b4b2f3999bcc0cc88a17721b70a2587a562fdf4 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 23 Mar 2020 06:18:59 -0700
Subject: [PATCH] [sledge] Add replay debugging for Equality

Summary:
This diff adds wrappers for Equality entry points that augment
exceptions escaping out of Equality with an sexp that can be given
back to Equality.replay in order to reexecute the function call that
failed.

A (bogus) example could be raising:
```
((Failure "domains intersect: ((u8) %x_5)")
 (And_eq () (Ap1 (Unsigned (bits 8)) (Var (id 5) (name x)))
   (Var (id 6) (name y))
   ((xs ()) (sat true)
     (rep (((Var (id 6) (name y)) (Var (id 5) (name x))))))))
```
and then calling `Equality.replay {|(And_eq ...)|}`.

Reviewed By: jvillard

Differential Revision: D20583753

fbshipit-source-id: 80d855950
---
 sledge/lib/equality.ml      | 48 +++++++++++++++++++++++++++++++++++++
 sledge/lib/equality.mli     |  4 ++++
 sledge/lib/equality_test.ml | 12 +++++++---
 3 files changed, 61 insertions(+), 3 deletions(-)

diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml
index 6b9e6387b..84b0de9fa 100644
--- a/sledge/lib/equality.ml
+++ b/sledge/lib/equality.ml
@@ -1015,3 +1015,51 @@ let solve_for_vars vss r =
               then Stop true
               else Continue us_xs )
             ~finish:(fun _ -> false) ) )]
+
+(* Replay debugging *)
+
+type call =
+  | And_eq of Var.Set.t * Term.t * Term.t * t
+  | And_term of Var.Set.t * Term.t * t
+  | And_ of Var.Set.t * t * t
+  | Or_ of Var.Set.t * t * t
+  | OrN of Var.Set.t * t list
+  | Rename of t * Var.Subst.t
+  | Apply_subst of Var.Set.t * Subst.t * t
+  | Solve_for_vars of Var.Set.t list * t
+[@@deriving sexp]
+
+let replay c =
+  match call_of_sexp (Sexp.of_string c) with
+  | And_eq (us, a, b, r) -> and_eq us a b r |> ignore
+  | And_term (us, e, r) -> and_term us e r |> ignore
+  | And_ (us, r, s) -> and_ us r s |> ignore
+  | Or_ (us, r, s) -> or_ us r s |> ignore
+  | OrN (us, rs) -> orN us rs |> ignore
+  | Rename (r, s) -> rename r s |> ignore
+  | Apply_subst (us, s, r) -> apply_subst us s r |> ignore
+  | Solve_for_vars (vss, r) -> solve_for_vars vss r |> ignore
+
+(* Debug wrappers *)
+
+let wrap f call =
+  if not [%debug] then f ()
+  else
+    try f () with exn -> raise_s ([%sexp_of: exn * call] (exn, call ()))
+
+let and_eq us a b r =
+  wrap (fun () -> and_eq us a b r) (fun () -> And_eq (us, a, b, r))
+
+let and_term us e r =
+  wrap (fun () -> and_term us e r) (fun () -> And_term (us, e, r))
+
+let and_ us r s = wrap (fun () -> and_ us r s) (fun () -> And_ (us, r, s))
+let or_ us r s = wrap (fun () -> or_ us r s) (fun () -> Or_ (us, r, s))
+let orN us rs = wrap (fun () -> orN us rs) (fun () -> OrN (us, rs))
+let rename r s = wrap (fun () -> rename r s) (fun () -> Rename (r, s))
+
+let apply_subst us s r =
+  wrap (fun () -> apply_subst us s r) (fun () -> Apply_subst (us, s, r))
+
+let solve_for_vars vss r =
+  wrap (fun () -> solve_for_vars vss r) (fun () -> Solve_for_vars (vss, r))
diff --git a/sledge/lib/equality.mli b/sledge/lib/equality.mli
index ef0469241..ffae2a869 100644
--- a/sledge/lib/equality.mli
+++ b/sledge/lib/equality.mli
@@ -96,3 +96,7 @@ val solve_for_vars : Var.Set.t list -> t -> Subst.t
     with free variables contained in (the union of) a prefix [uss] of [vss]
     to terms [e] with free variables contained in as short a prefix of [uss]
     as possible. *)
+
+(* Replay debugging *)
+
+val replay : string -> unit
diff --git a/sledge/lib/equality_test.ml b/sledge/lib/equality_test.ml
index 4d0c22654..a0f468d9f 100644
--- a/sledge/lib/equality_test.ml
+++ b/sledge/lib/equality_test.ml
@@ -5,8 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-(* [@@@warning "-32"] *)
-
 let%test_module _ =
   ( module struct
     open Equality
@@ -16,7 +14,9 @@ let%test_module _ =
     (* let () =
      *   Trace.init ~margin:160
      *     ~config:(Result.ok_exn (Trace.parse "+Equality"))
-     *     () *)
+     *     ()
+     * 
+     * [@@@warning "-32"] *)
 
     let printf pp = Format.printf "@\n%a@." pp
     let pp = printf pp
@@ -410,4 +410,10 @@ let%test_module _ =
         {| {sat= true; rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]]} |}]
 
     let%test _ = entails_eq r19 z !0
+
+    let%expect_test _ =
+      Equality.replay
+        {|(Solve_for_vars (() () ((Var (id 8) (name m)) (Var (id 9) (name n))))
+           ((xs ()) (sat true) (rep (((Var (id 9) (name n)) (Var (id 8) (name m)))))))|} ;
+      [%expect {||}]
   end )