[sledge] Add support for dumping and replaying solver queries

Reviewed By: jvillard

Differential Revision: D25756552

fbshipit-source-id: b73a4fc98

sledge/cli/sledge_cli.ml

@@ -118,6 +118,9 @@ let analyze =
       ~doc:"do not simplify states during symbolic execution"
   and stats =
     flag "stats" no_arg ~doc:"output performance statistics to stderr"
+  and dump_query =
+    flag "dump-query" (optional int)
+      ~doc:"<int> dump solver query <int> and halt"
   in
   fun program () ->
     Timer.enabled := stats ;
@@ -139,6 +142,7 @@ let analyze =
     let module Dom = (val dom) in
     let module Analysis = Control.Make (Opts) (Dom) in
     Domain_sh.simplify_states := not no_simplify_states ;
+    Option.iter dump_query ~f:(fun n -> Solver.dump_query := n) ;
     Analysis.exec_pgm pgm ;
     Report.coverage pgm ;
     Report.safe_or_unsafe ()

sledge/sledge-help.txt

@@ -53,6 +53,7 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s
   [-domain <string>]     select abstract domain; must be one of "sh" (default,
                          symbolic heap domain), "globals" (used-globals domain),
                          or "unit" (unit domain)
+  [-dump-query <int>]    dump solver query <int> and halt
   [-function-summaries]  use function summaries (in development)
   [-fuzzer]              add a harness for libFuzzer targets
   [-margin <cols>]       wrap debug tracing at <cols> columns
@@ -150,6 +151,7 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo
   [-domain <string>]     select abstract domain; must be one of "sh" (default,
                          symbolic heap domain), "globals" (used-globals domain),
                          or "unit" (unit domain)
+  [-dump-query <int>]    dump solver query <int> and halt
   [-function-summaries]  use function summaries (in development)
   [-fuzzer]              add a harness for libFuzzer targets
   [-margin <cols>]       wrap debug tracing at <cols> columns
@@ -236,6 +238,7 @@ The <input> file must be binary LLAIR, such as produced by `sledge translate`.
   [-domain <string>]     select abstract domain; must be one of "sh" (default,
                          symbolic heap domain), "globals" (used-globals domain),
                          or "unit" (unit domain)
+  [-dump-query <int>]    dump solver query <int> and halt
   [-function-summaries]  use function summaries (in development)
   [-margin <cols>]       wrap debug tracing at <cols> columns
   [-no-simplify-states]  do not simplify states during symbolic execution

sledge/src/solver.ml

@@ -674,12 +674,14 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
       in
       Sh.or_ remainders remainder )
 
+let query_count = ref (-1)
+
 let infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
  fun minuend xs subtrahend ->
   [%trace]
     ~call:(fun {pf} ->
-      pf "@ @[<hv>%a@ \\- %a%a@]" Sh.pp minuend Var.Set.pp_xs xs Sh.pp
+      pf " %i@ @[<hv>%a@ \\- %a%a@]" !query_count Sh.pp minuend
-        subtrahend )
+        Var.Set.pp_xs xs Sh.pp subtrahend )
     ~retn:(fun {pf} r ->
       pf "%a" (Option.pp "%a" Sh.pp) r ;
       Option.iter r ~f:(fun frame ->
@@ -695,3 +697,24 @@ let infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
   assert (Var.Set.subset xs ~of_:subtrahend.us) ;
   assert (Var.Set.subset (Var.Set.diff subtrahend.us xs) ~of_:minuend.us) ;
   excise_dnf minuend xs subtrahend
+
+(*
+ * Replay debugging
+ *)
+
+type call = Infer_frame of Sh.t * Var.Set.t * Sh.t [@@deriving sexp]
+
+let replay c =
+  match call_of_sexp (Sexp.of_string c) with
+  | Infer_frame (minuend, xs, subtrahend) ->
+      infer_frame minuend xs subtrahend |> ignore
+
+let dump_query = ref (-1)
+
+let infer_frame minuend xs subtrahend =
+  Int.incr query_count ;
+  if !query_count = !dump_query then
+    fail "%a" Sexp.pp_hum
+      (sexp_of_call (Infer_frame (minuend, xs, subtrahend)))
+      ()
+  else infer_frame minuend xs subtrahend

sledge/src/solver.mli

@@ -15,3 +15,8 @@ val infer_frame : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option
     to be strong enough that for every model of [r], there exists an
     extension of it satisfying [q], such that the combination (with [xs]
     projected out) satisfies [p]. *)
+
+(**/**)
+
+val dump_query : int ref
+val replay : string -> unit

sledge/src/test/solver_test.ml

@@ -59,21 +59,21 @@ let%test_module _ =
       check_frame Sh.emp [] Sh.emp ;
       [%expect
         {|
-        ( infer_frame:   emp \-   emp
+        ( infer_frame: 0   emp \-   emp
         ) infer_frame:   emp |}]
 
     let%expect_test _ =
       check_frame (Sh.false_ Var.Set.empty) [] Sh.emp ;
       [%expect
         {|
-        ( infer_frame: false \-   emp
+        ( infer_frame: 1 false \-   emp
         ) infer_frame: false |}]
 
     let%expect_test _ =
       check_frame Sh.emp [n_; m_] (Sh.and_ (Formula.eq m n) Sh.emp) ;
       [%expect
         {|
-        ( infer_frame:   emp \- ∃ %m_8, %n_9 .   %m_8 = %n_9 ∧ emp
+        ( infer_frame: 2   emp \- ∃ %m_8, %n_9 .   %m_8 = %n_9 ∧ emp
         ) infer_frame:   %m_8 = %n_9 ∧ emp |}]
 
     let%expect_test _ =
@@ -82,7 +82,7 @@ let%test_module _ =
         [] Sh.emp ;
       [%expect
         {|
-        ( infer_frame:   %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ \-   emp
+        ( infer_frame: 3   %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ \-   emp
         ) infer_frame:   %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩ |}]
 
     let%expect_test _ =
@@ -92,7 +92,7 @@ let%test_module _ =
         (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ;
       [%expect
         {|
-        ( infer_frame:
+        ( infer_frame: 4
             %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩
           \-   %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩
         ) infer_frame:   emp |}]
@@ -110,7 +110,7 @@ let%test_module _ =
       infer_frame minued [n_; m_] subtrahend ;
       [%expect
         {|
-        ( infer_frame:
+        ( infer_frame: 5
             %l_6 -[ %b_4, 10 )-> ⟨10,%a_1⟩ * %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩
           \- ∃ %m_8, %n_9 .
             ∃ %m_10 .   %m_8 = %n_9 ∧ %l_7 -[ %b_4, 10 )-> ⟨10,%a_2⟩
@@ -126,7 +126,7 @@ let%test_module _ =
         (Sh.seg {loc= l; bas= b; len= m; siz= n; cnt= a}) ;
       [%expect
         {|
-        ( infer_frame:
+        ( infer_frame: 6
             %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩
           * %l_7 -[ %b_4, %m_8 )-> ⟨%n_9,%a_2⟩
           \-   %l_6 -[ %b_4, %m_8 )-> ⟨%n_9,%a_1⟩
@@ -141,7 +141,7 @@ let%test_module _ =
         (Sh.seg {loc= l; bas= l; len= !16; siz= !16; cnt= a3}) ;
       [%expect
         {|
-        ( infer_frame:
+        ( infer_frame: 7
             %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3 .   %l_6 -[)-> ⟨16,%a_3⟩
         ) infer_frame:   (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}]
 
@@ -154,7 +154,7 @@ let%test_module _ =
         (Sh.seg {loc= l; bas= l; len= m; siz= !16; cnt= a3}) ;
       [%expect
         {|
-        ( infer_frame:
+        ( infer_frame: 8
             %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩
@@ -169,7 +169,7 @@ let%test_module _ =
         (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a3}) ;
       [%expect
         {|
-        ( infer_frame:
+        ( infer_frame: 9
             %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩
           \- ∃ %a_3, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩
@@ -186,7 +186,7 @@ let%test_module _ =
            (Sh.seg {loc= k; bas= k; len= m; siz= n; cnt= a2})) ;
       [%expect
         {|
-        ( infer_frame:
+        ( infer_frame: 10
             %k_5 -[ %k_5, 16 )-> ⟨32,%a_1⟩ * %l_6 -[)-> ⟨8,16⟩
           \- ∃ %a_2, %m_8, %n_9 .
               %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩
@@ -208,7 +208,7 @@ let%test_module _ =
            (Sh.seg {loc= l; bas= l; len= !8; siz= !8; cnt= n})) ;
       [%expect
         {|
-        ( infer_frame:
+        ( infer_frame: 11
             %k_5 -[ %k_5, 16 )-> ⟨32,%a_1⟩ * %l_6 -[)-> ⟨8,16⟩
           \- ∃ %a_2, %m_8, %n_9 .
               %k_5 -[ %k_5, %m_8 )-> ⟨%n_9,%a_2⟩ * %l_6 -[)-> ⟨8,%n_9⟩
@@ -234,7 +234,7 @@ let%test_module _ =
         (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ;
       [%expect
         {|
-        ( infer_frame:
+        ( infer_frame: 12
             %l_6 -[ %l_6, 16 )-> ⟨8×%n_9,%a_2⟩^⟨(16 + -8×%n_9),%a_3⟩
           * ( (  0 = %n_9 ∧ emp)
             ∨ (  1 = %n_9 ∧ emp)
@@ -259,7 +259,7 @@ let%test_module _ =
         (Sh.seg {loc= l; bas= l; len= m; siz= m; cnt= a}) ;
       [%expect
         {|
-        ( infer_frame:
+        ( infer_frame: 13
             (2 ≥ %n_9)
           ∧ %l_6 -[ %l_6, 16 )-> ⟨8×%n_9,%a_2⟩^⟨(16 + -8×%n_9),%a_3⟩
           \- ∃ %a_1, %m_8 .
@@ -276,6 +276,7 @@ let%test_module _ =
       infer_frame minuend [m_] subtrahend ;
       [%expect
         {|
-        ( infer_frame:   emp \- ∃ %m_8 .   %a_1 = %m_8 ∧ (0 ≠ %a_1) ∧ emp
+        ( infer_frame: 14
+            emp \- ∃ %m_8 .   %a_1 = %m_8 ∧ (0 ≠ %a_1) ∧ emp
         ) infer_frame: |}]
   end )