From 15300403a5caafaa62c7f83cfe2e5984cee1eb7e Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 19 Mar 2019 09:26:05 -0700 Subject: [PATCH] [sledge] Improve debug tracing Reviewed By: jvillard Differential Revision: D14427775 fbshipit-source-id: ddc7d3647 --- sledge/src/llair/exp.ml | 8 +++--- sledge/src/llair/exp_test.ml | 4 +-- sledge/src/symbheap/equality.ml | 2 +- sledge/src/symbheap/exec.ml | 2 +- sledge/src/symbheap/sh.ml | 27 ++++++++++++++------ sledge/src/symbheap/sh.mli | 2 ++ sledge/src/symbheap/solver.ml | 40 ++++++++++++++++-------------- sledge/src/symbheap/solver_test.ml | 8 +----- 8 files changed, 51 insertions(+), 42 deletions(-) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index d4c266807..a20c0a2eb 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -263,13 +263,13 @@ let rec pp fs exp = | Eq -> pf "=" | Dq -> pf "@<1>≠" | Gt -> pf ">" - | Ge -> pf ">=" + | Ge -> pf "@<1>≥" | Lt -> pf "<" - | Le -> pf "<=" + | Le -> pf "@<1>≤" | Ugt -> pf "u>" - | Uge -> pf "u>=" + | Uge -> pf "@<2>u≥" | Ult -> pf "u<" - | Ule -> pf "u<=" + | Ule -> pf "@<2>u≤" | Ord -> pf "ord" | Uno -> pf "uno" | Add {args} -> diff --git a/sledge/src/llair/exp_test.ml b/sledge/src/llair/exp_test.ml index e98f958dc..05b8ba270 100644 --- a/sledge/src/llair/exp_test.ml +++ b/sledge/src/llair/exp_test.ml @@ -237,11 +237,11 @@ let%test_module _ = let%expect_test _ = pp ~~(y > !2 && z <= !3) ; - [%expect {| ((%y_1 <= 2) || (%z_2 > 3)) |}] + [%expect {| ((%y_1 ≤ 2) || (%z_2 > 3)) |}] let%expect_test _ = pp ~~(y >= !2 || z < !3) ; - [%expect {| ((%y_1 < 2) && (%z_2 >= 3)) |}] + [%expect {| ((%y_1 < 2) && (%z_2 ≥ 3)) |}] let%expect_test _ = pp Exp.(eq z null) ; diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml index 8b30a2a9f..8a9ce6f81 100644 --- a/sledge/src/symbheap/equality.ml +++ b/sledge/src/symbheap/equality.ml @@ -224,7 +224,7 @@ let difference r a b = | _ -> None ) |> [%Trace.retn fun {pf} -> - function Some d -> pf "%a" Z.pp_print d | None -> ()] + function Some d -> pf "%a" Z.pp_print d | None -> pf ""] let and_ r s = if not r.sat then r diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index ba55e9f00..0d6678011 100644 --- a/sledge/src/symbheap/exec.ml +++ b/sledge/src/symbheap/exec.ml @@ -451,7 +451,7 @@ let strlen_spec us reg ptr = (* execute a command with given spec from pre *) let exec_spec pre {xs; foot; post} = [%Trace.call fun {pf} -> - pf "@[%a@]@ @[<2>%a@,@[{%a }@;<1 -1>-- {%a }@]@]" Sh.pp pre + pf "@[%a@]@ @[<2>%a@\n@[{%a }@;<1 -1>--@ {%a }@]@]" Sh.pp pre (Sh.pp_us ~pre:"@<2>∀ ") xs Sh.pp foot Sh.pp post ; assert ( diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 0d72dec10..025175eab 100644 --- a/sledge/src/symbheap/sh.ml +++ b/sledge/src/symbheap/sh.ml @@ -35,16 +35,22 @@ let pp_seg fs {loc; bas; len; siz; arr} = Format.fprintf fs " %a, %a " Exp.pp bas Exp.pp len ) (bas, len) Exp.pp (Exp.memory ~siz ~arr) +let pp_seg_norm cong fs seg = + pp_seg fs (map_seg seg ~f:(Equality.normalize cong)) + let pp_us ?(pre = ("" : _ fmt)) fs us = if not (Set.is_empty us) then [%Trace.fprintf fs "%( %)@[%a@] .@ " pre Var.Set.pp us] -let rec pp_ vs fs {us; xs; cong; pure; heap; djns} = +let rec pp vs fs {us; xs; cong; pure; heap; djns} = Format.pp_open_hvbox fs 0 ; pp_us fs us ; - if not (Set.is_empty xs) then - Format.fprintf fs "@<2>∃ @[%a@] .@ ∃ @[%a@] .@ " Var.Set.pp - (Set.inter xs vs) Var.Set.pp (Set.diff xs vs) ; + let xs_i_vs, xs_d_vs = Set.inter_diff vs xs in + if not (Set.is_empty xs_i_vs) then ( + Format.fprintf fs "@<2>∃ @[%a@] ." Var.Set.pp xs_i_vs ; + if not (Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ; + if not (Set.is_empty xs_d_vs) then + Format.fprintf fs "@<2>∃ @[%a@] .@ " Var.Set.pp xs_d_vs ; let first = Equality.is_true cong in if not first then Format.fprintf fs " " ; Equality.pp_classes fs cong ; @@ -84,11 +90,12 @@ and pp_djn vs fs = function | djn -> Format.fprintf fs "@[( %a@ )@]" (List.pp "@ @<2>∨ " (fun fs sjn -> - Format.fprintf fs "@[(%a)@]" (pp_ vs) + Format.fprintf fs "@[(%a)@]" (pp vs) {sjn with us= Set.diff sjn.us vs} )) djn -let pp = pp_ Var.Set.empty +let pp = pp Var.Set.empty +let pp_djn = pp_djn Var.Set.empty let fold_exps_seg {loc; bas; len; siz; arr} ~init ~f = let f b z = Exp.fold_exps b ~init:z ~f in @@ -269,7 +276,7 @@ let and_cong cong q = [%Trace.retn fun {pf} q -> pf "%a" pp q ; invariant q] let star q1 q2 = - [%Trace.call fun {pf} -> pf "%a@ %a" pp q1 pp q2] + [%Trace.call fun {pf} -> pf "(%a)@ (%a)" pp q1 pp q2] ; ( match (q1, q2) with | {djns= [[]]; _}, _ | _, {djns= [[]]; _} -> @@ -305,7 +312,7 @@ let star q1 q2 = assert (Set.equal q.us (Set.union q1.us q2.us))] let or_ q1 q2 = - [%Trace.call fun {pf} -> pf "%a@ %a" pp q1 pp q2] + [%Trace.call fun {pf} -> pf "(%a)@ (%a)" pp q1 pp q2] ; ( match (q1, q2) with | {djns= [[]]; _}, _ -> @@ -406,6 +413,8 @@ let fold_dnf ~conj ~disj sjn conjuncts disjuncts = add_disjunct [] sjn (conjuncts, disjuncts) let dnf q = + [%Trace.call fun {pf} -> pf "%a" pp q] + ; let conj sjn conjuncts = assert (List.is_empty sjn.djns) ; assert (List.is_empty conjuncts.djns) ; @@ -416,3 +425,5 @@ let dnf q = conjuncts :: disjuncts in fold_dnf ~conj ~disj q emp [] + |> + [%Trace.retn fun {pf} -> pf "%a" pp_djn] diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli index f6015ab2c..37999ef53 100644 --- a/sledge/src/symbheap/sh.mli +++ b/sledge/src/symbheap/sh.mli @@ -26,8 +26,10 @@ and disjunction = starjunction list type t = starjunction val pp_seg : seg pp +val pp_seg_norm : Equality.t -> seg pp val pp_us : ?pre:('a, 'a) fmt -> Var.Set.t pp val pp : t pp +val pp_djn : disjunction pp include Invariant.S with type t := t diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml index e6fed561e..ac328b3ea 100644 --- a/sledge/src/symbheap/solver.ml +++ b/sledge/src/symbheap/solver.ml @@ -97,8 +97,8 @@ let excise_pure ({sub} as goal) = *) let excise_seg_same ({com; min; sub} as goal) msg ssg = [%Trace.info - "@[excise_seg_same@ %a@ %a@ %a@]" Sh.pp_seg msg Sh.pp_seg ssg pp - goal] ; + "@[excise_seg_same@ %a@ %a@ %a@]" (Sh.pp_seg_norm sub.cong) msg + (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.bas= b; len= m; arr= a} = msg in let {Sh.bas= b'; len= m'; arr= a'} = ssg in let com = Sh.star (Sh.seg msg) com in @@ -125,8 +125,8 @@ let excise_seg_same ({com; min; sub} as goal) msg ssg = let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n = [%Trace.info - "@[excise_seg_sub_prefix@ %a@ %a@ %a@]" Sh.pp_seg msg Sh.pp_seg - ssg pp goal] ; + "@[excise_seg_sub_prefix@ %a@ %a@ %a@]" (Sh.pp_seg_norm sub.cong) + msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.bas= b'; len= m'; siz= n; arr= a'} = ssg in let o_n = Exp.integer o_n Typ.siz in @@ -167,8 +167,8 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o = [%Trace.info - "@[excise_seg_min_prefix@ %a@ %a@ %a@]" Sh.pp_seg msg Sh.pp_seg - ssg pp goal] ; + "@[excise_seg_min_prefix@ %a@ %a@ %a@]" (Sh.pp_seg_norm sub.cong) + msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let n_o = Exp.integer n_o Typ.siz in @@ -210,8 +210,8 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k = [%Trace.info - "@[excise_seg_sub_suffix@ %a@ %a@ %a@]" Sh.pp_seg msg Sh.pp_seg - ssg pp goal] ; + "@[excise_seg_sub_suffix@ %a@ %a@ %a@]" (Sh.pp_seg_norm sub.cong) + msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let l_k = Exp.integer l_k Typ.siz in @@ -253,8 +253,8 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k ko_ln = [%Trace.info - "@[excise_seg_sub_infix@ %a@ %a@ %a@]" Sh.pp_seg msg Sh.pp_seg ssg - pp goal] ; + "@[excise_seg_sub_infix@ %a@ %a@ %a@]" (Sh.pp_seg_norm sub.cong) + msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let l_k = Exp.integer l_k Typ.siz and ko_ln = Exp.integer ko_ln Typ.siz in @@ -302,8 +302,8 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k ko_l ln_ko = [%Trace.info - "@[excise_seg_min_skew@ %a@ %a@ %a@]" Sh.pp_seg msg Sh.pp_seg ssg - pp goal] ; + "@[excise_seg_min_skew@ %a@ %a@ %a@]" (Sh.pp_seg_norm sub.cong) + msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let l_k = Exp.integer l_k Typ.siz in @@ -358,8 +358,8 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l = [%Trace.info - "@[excise_seg_min_suffix@ %a@ %a@ %a@]" Sh.pp_seg msg Sh.pp_seg - ssg pp goal] ; + "@[excise_seg_min_suffix@ %a@ %a@ %a@]" (Sh.pp_seg_norm sub.cong) + msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let k_l = Exp.integer k_l Typ.siz in @@ -398,8 +398,8 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l ln_ko = [%Trace.info - "@[excise_seg_min_infix@ %a@ %a@ %a@]" Sh.pp_seg msg Sh.pp_seg ssg - pp goal] ; + "@[excise_seg_min_infix@ %a@ %a@ %a@]" (Sh.pp_seg_norm sub.cong) + msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let k_l = Exp.integer k_l Typ.siz in @@ -444,8 +444,8 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l ln_k ko_ln = [%Trace.info - "@[excise_seg_sub_skew@ %a@ %a@ %a@]" Sh.pp_seg msg Sh.pp_seg ssg - pp goal] ; + "@[excise_seg_sub_skew@ %a@ %a@ %a@]" (Sh.pp_seg_norm sub.cong) + msg (Sh.pp_seg_norm sub.cong) ssg pp goal] ; let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in let k_l = Exp.integer k_l Typ.siz in @@ -485,7 +485,9 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l (* C ❮ k-[b;m)->⟨o,α⟩ * M ⊢ ∃xs. l-[b';m')->⟨n,α'⟩ * S ❯ R *) let excise_seg ({sub} as goal) msg ssg = - [%Trace.info "@[<2>excise_seg@ %a@ |- %a@]" Sh.pp_seg msg Sh.pp_seg ssg] ; + [%Trace.info + "@[<2>excise_seg@ %a@ |- %a@]" (Sh.pp_seg_norm sub.cong) msg + (Sh.pp_seg_norm sub.cong) ssg] ; let {Sh.loc= k; bas= b; len= m; siz= o} = msg in let {Sh.loc= l; bas= b'; len= m'; siz= n} = ssg in Equality.difference sub.cong k l diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml index 56ed6ff76..c0da338a0 100644 --- a/sledge/src/symbheap/solver_test.ml +++ b/sledge/src/symbheap/solver_test.ml @@ -103,11 +103,7 @@ let%test_module _ = \- ∃ %a_3 . %l_5 -[)-> ⟨16,%a_3⟩ ) infer_frame: - ∃ . - ∃ %a1_6 . - ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a1_6⟩ - ∧ %a_2 = %a1_6 - ∧ emp |}] + ∃ %a1_6 . ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a1_6⟩ ∧ %a_2 = %a1_6 ∧ emp |}] let%expect_test _ = check_frame @@ -124,7 +120,6 @@ let%test_module _ = \- ∃ %a_3, %m_7 . %l_5 -[ %l_5, %m_7 )-> ⟨16,%a_3⟩ ) infer_frame: - ∃ . ∃ %a1_8 . ⟨16,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a1_8⟩ ∧ %a_2 = %a1_8 @@ -146,7 +141,6 @@ let%test_module _ = \- ∃ %a_3, %m_7 . %l_5 -[)-> ⟨%m_7,%a_3⟩ ) infer_frame: - ∃ . ∃ %a1_8 . ⟨%m_7,%a_3⟩ = ⟨8,%a_1⟩^⟨8,%a1_8⟩ ∧ %a_2 = %a1_8