From 5c5a1cc58121e3bc1ad78b2fedca383fa7c4d618 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 12 Jan 2021 04:28:34 -0800 Subject: [PATCH] [sledge] Add support for dumping and replaying solver queries Reviewed By: jvillard Differential Revision: D25756552 fbshipit-source-id: b73a4fc98 --- sledge/cli/sledge_cli.ml | 4 ++++ sledge/sledge-help.txt | 3 +++ sledge/src/solver.ml | 27 +++++++++++++++++++++++++-- sledge/src/solver.mli | 5 +++++ sledge/src/test/solver_test.ml | 31 ++++++++++++++++--------------- 5 files changed, 53 insertions(+), 17 deletions(-) diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml index c4585f20e..63198d09b 100644 --- a/sledge/cli/sledge_cli.ml +++ b/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:" dump solver query 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 () diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 860d1685a..0349a83e6 100644 --- a/sledge/sledge-help.txt +++ b/sledge/sledge-help.txt @@ -53,6 +53,7 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s [-domain ] select abstract domain; must be one of "sh" (default, symbolic heap domain), "globals" (used-globals domain), or "unit" (unit domain) + [-dump-query ] dump solver query and halt [-function-summaries] use function summaries (in development) [-fuzzer] add a harness for libFuzzer targets [-margin ] wrap debug tracing at columns @@ -150,6 +151,7 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo [-domain ] select abstract domain; must be one of "sh" (default, symbolic heap domain), "globals" (used-globals domain), or "unit" (unit domain) + [-dump-query ] dump solver query and halt [-function-summaries] use function summaries (in development) [-fuzzer] add a harness for libFuzzer targets [-margin ] wrap debug tracing at columns @@ -236,6 +238,7 @@ The file must be binary LLAIR, such as produced by `sledge translate`. [-domain ] select abstract domain; must be one of "sh" (default, symbolic heap domain), "globals" (used-globals domain), or "unit" (unit domain) + [-dump-query ] dump solver query and halt [-function-summaries] use function summaries (in development) [-margin ] wrap debug tracing at columns [-no-simplify-states] do not simplify states during symbolic execution diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml index 177d3a3a2..86f27c545 100644 --- a/sledge/src/solver.ml +++ b/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 "@ @[%a@ \\- %a%a@]" Sh.pp minuend Var.Set.pp_xs xs Sh.pp - subtrahend ) + pf " %i@ @[%a@ \\- %a%a@]" !query_count Sh.pp minuend + 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 diff --git a/sledge/src/solver.mli b/sledge/src/solver.mli index ae6ae86ca..1a569551e 100644 --- a/sledge/src/solver.mli +++ b/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 diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml index 2de7aff7c..576011588 100644 --- a/sledge/src/test/solver_test.ml +++ b/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 )