From 239d906ab659c0f64434edd13dde2b63ea87f1c5 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 14 Oct 2019 07:24:20 -0700 Subject: [PATCH] [sledge] Improve tracing and debugging support Reviewed By: ngorogiannis Differential Revision: D17801930 fbshipit-source-id: 8cfac2eaf --- sledge/src/control.ml | 2 +- sledge/src/llair/term.ml | 2 +- sledge/src/symbheap/exec.ml | 45 ++++++++++++++++++++++++++----------- sledge/src/symbheap/sh.ml | 16 ++++++++----- 4 files changed, 45 insertions(+), 20 deletions(-) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 54fc55766..4b7c9e1d5 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -274,7 +274,7 @@ module Make (Dom : Domain_sig.Dom) = struct let Llair.{callee; actuals; areturn; return; recursive} = call in let Llair.{name; formals; freturn; locals; entry} = callee in [%Trace.call fun {pf} -> - pf "%a from %a with state %a" Reg.pp name.reg Reg.pp + pf "%a from %a with state@ %a" Reg.pp name.reg Reg.pp return.dst.parent.name.reg Dom.pp state] ; let dnf_states = diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml index c69bae17e..12ea82932 100644 --- a/sledge/src/llair/term.ml +++ b/sledge/src/llair/term.ml @@ -428,7 +428,7 @@ module Var = struct let pp fs s = Format.fprintf fs "@[<1>[%a]@]" (List.pp ",@ " (fun fs (k, v) -> - Format.fprintf fs "@[[%a ↦ %a]@]" pp_t k pp_t v )) + Format.fprintf fs "@[%a ↦ %a@]" pp_t k pp_t v )) (Map.to_alist s) let empty = empty_map diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index 1002f761d..b6024d745 100644 --- a/sledge/src/symbheap/exec.ml +++ b/sledge/src/symbheap/exec.ml @@ -646,10 +646,16 @@ let strlen_spec us reg ptr = * Symbolic Execution *) +let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) = + let gain_us = Set.diff q1.us q0.us in + let lose_us = Set.diff q0.us q1.us in + (Set.is_empty gain_us || fail "gain us: %a" Var.Set.pp gain_us ()) + && (Set.is_empty lose_us || fail "lose us: %a" Var.Set.pp lose_us ()) + (* execute a command with given spec from pre *) -let exec_spec pre {xs; foot; sub; ms; post} = +let exec_spec pre0 {xs; foot; sub; ms; post} = [%Trace.call fun {pf} -> - pf "@[%a@]@ @[<2>%a@,@[{%a %a}@;<1 -1>%a--@ {%a }@]@]" Sh.pp pre + pf "@[%a@]@ @[<2>%a@,@[{%a %a}@;<1 -1>%a--@ {%a }@]@]" Sh.pp pre0 (Sh.pp_us ~pre:"@<2>∀ ") xs Sh.pp foot (fun fs sub -> @@ -661,20 +667,22 @@ let exec_spec pre {xs; foot; sub; ms; post} = Format.fprintf fs "%a := " Var.Set.pp ms ) ms Sh.pp post ; assert ( - let vs = Set.diff (Set.diff foot.us xs) pre.us in + let vs = Set.diff (Set.diff foot.us xs) pre0.us in Set.is_empty vs || fail "unbound foot: {%a}" Var.Set.pp vs () ) ; assert ( - let vs = Set.diff (Set.diff post.us xs) pre.us in + let vs = Set.diff (Set.diff post.us xs) pre0.us in Set.is_empty vs || fail "unbound post: {%a}" Var.Set.pp vs () )] ; let foot = Sh.extend_us xs foot in - let zs, pre = Sh.bind_exists pre ~wrt:xs in + let zs, pre = Sh.bind_exists pre0 ~wrt:xs in ( Solver.infer_frame pre xs foot >>| fun frame -> Sh.exists (Set.union zs xs) (Sh.star post (Sh.exists ms (Sh.rename sub frame))) ) |> - [%Trace.retn fun {pf} r -> pf "%a" (Option.pp "%a" Sh.pp) r] + [%Trace.retn fun {pf} r -> + pf "%a" (Option.pp "%a" Sh.pp) r ; + assert (Option.for_all ~f:(check_preserve_us pre0) r)] (* execute a multiple-spec command, where the disjunction of the specs preconditions are known to be tautologous *) @@ -687,6 +695,14 @@ let rec exec_specs pre = function exec_specs pre specs >>| fun posts -> Sh.or_ post posts | [] -> Some (Sh.false_ pre.us) +let exec_specs pre specs = + [%Trace.call fun _ -> ()] + ; + exec_specs pre specs + |> + [%Trace.retn fun _ r -> + assert (Option.for_all ~f:(check_preserve_us pre) r)] + (* * Exposed interface *) @@ -723,18 +739,13 @@ let abort _ = None let intrinsic ~skip_throw : Sh.t -> Var.t option -> Var.t -> Term.t list -> Sh.t option option = fun pre areturn intrinsic actuals -> - [%Trace.info - "@[<2>exec intrinsic@ @[%a%a(@[%a@])@] from@ @[{ %a@ }@]@]" - (Option.pp "%a := " Var.pp) - areturn Var.pp intrinsic (List.pp ",@ " Term.pp) (List.rev actuals) - Sh.pp pre] ; let us = pre.us in let name = let n = Var.name intrinsic in match String.index n '.' with None -> n | Some i -> String.prefix n i in let skip pre = Some (Some pre) in - match (areturn, name, actuals) with + ( match (areturn, name, actuals) with (* * cstdlib - memory management *) @@ -808,4 +819,12 @@ let intrinsic ~skip_throw : *) (* bool folly::usingJEMalloc() *) | Some _, "_ZN5folly13usingJEMallocEv", [] -> skip pre - | _ -> None + | _ -> None ) + $> function + | None -> () + | Some _ -> + [%Trace.info + "@[<2>exec intrinsic@ @[%a%a(@[%a@])@] from@ @[{ %a@ }@]@]" + (Option.pp "%a := " Var.pp) + areturn Var.pp intrinsic (List.pp ",@ " Term.pp) + (List.rev actuals) Sh.pp pre] diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 67c82a92c..dc841184f 100644 --- a/sledge/src/symbheap/sh.ml +++ b/sledge/src/symbheap/sh.ml @@ -240,11 +240,11 @@ and freshen_xs q ~wrt = if xs == q.xs && q' == q then q else {q' with xs} ) |> [%Trace.retn fun {pf} q' -> - pf "%a" pp q' ; - invariant q' ; + pf "%a@ %a" Var.Subst.pp sub pp q' ; assert (Set.equal q'.us q.us) ; assert (Set.disjoint q'.xs (Var.Subst.domain sub)) ; - assert (Set.disjoint q'.xs (Set.inter q.xs wrt))] + assert (Set.disjoint q'.xs (Set.inter q.xs wrt)) ; + invariant q'] let extend_us us q = let us = Set.union us q.us in @@ -273,8 +273,7 @@ let exists xs q = ; assert ( Set.is_subset xs ~of_:q.us - || fail "Sh.exists fail xs - q.us:%a" Var.Set.pp (Set.diff xs q.us) () - ) ; + || fail "Sh.exists xs - q.us: %a" Var.Set.pp (Set.diff xs q.us) () ) ; {q with us= Set.diff q.us xs; xs= Set.union q.xs xs} |> check invariant |> [%Trace.retn fun {pf} -> pf "%a" pp] @@ -440,6 +439,13 @@ let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) = if heap == q.heap && djns == q.djns then q else {us; xs; cong; pure; heap; djns} |> check invariant +let pure_approx q = + [%Trace.call fun {pf} -> pf "%a" pp q] + ; + pure_approx q + |> + [%Trace.retn fun {pf} -> pf "%a" pp] + let fold_dnf ~conj ~disj sjn (xs, conjuncts) disjuncts = let rec add_disjunct pending_splits sjn (xs, conjuncts) disjuncts = let ys, sjn = bind_exists sjn ~wrt:xs in