[sledge] Improve debug tracing

Reviewed By: mbouaziz

Differential Revision: D10389475

fbshipit-source-id: 28df69903

sledge/src/control.ml

@@ -163,7 +163,23 @@ let exec_throw stk state block exc =
       exec_jump stk state block {jmp with args= exc :: args}
   | None -> Work.skip
 
-let exec_skip_func stk state block ({dst; args} as return : Llair.jump) =
+let exec_skip_func :
+    stack -> Domain.t -> Llair.block -> Llair.jump -> Work.x =
+ fun stk state block ({dst; args} as return) ->
+  Format.eprintf
+    "@\n\
+     @[<v 2>%a Called unknown function %a executing instruction@;<1 \
+     2>@[%a@]@]@."
+    Loc.pp
+    (Llair.Term.loc block.term)
+    (fun fs (term : Llair.Term.t) ->
+      match term with
+      | Call {call= {dst}} -> (
+        match Var.of_exp dst with
+        | Some var -> Var.pp_demangled fs var
+        | None -> Exp.pp fs dst )
+      | _ -> () )
+    block.term Llair.Term.pp block.term ;
   let return =
     if List.is_empty dst.params then return
     else

sledge/src/llair/exp.ml

@@ -93,7 +93,7 @@ module T = struct
     in
     uncurry_ []
 
-  let pp fs exp =
+  let rec pp fs exp =
     let pp_ pp fs exp =
       let pf fmt =
         Format.pp_open_box fs 2 ;
@@ -158,13 +158,29 @@ module T = struct
       | Record -> pf "{_}"
       | App {op; arg} -> (
         match uncurry exp with
-        | Record, elts -> pf "{@[%a@]}" (List.pp ",@ " pp) elts
+        | Record, elts -> pf "{%a}" pp_record elts
         | op, [x; y] -> pf "(%a@ %a %a)" pp x pp op pp y
         | _ -> pf "(%a@ %a)" pp op pp arg )
       | Struct_rec {elts} -> pf "{|%a|}" (Vector.pp ",@ " pp) elts
       | Convert {dst; src} -> pf "(%a)(%a)" Typ.pp dst Typ.pp src
     in
     fix_flip pp_ (fun _ _ -> ()) fs exp
+
+  and pp_record fs elts =
+    [%Trace.fprintf
+      fs "%a"
+        (fun fs elts ->
+          let elta = Array.of_list elts in
+          match
+            String.init (Array.length elta) ~f:(fun i ->
+                match elta.(i) with
+                | Integer {data} -> Char.of_int_exn (Z.to_int data)
+                | _ -> raise (Invalid_argument "not a string") )
+          with
+          | s -> Format.fprintf fs "@[<h>%s@]" (String.escaped s)
+          | exception _ ->
+              Format.fprintf fs "@[<h>%a@]" (List.pp ",@ " pp) elts )
+        elts]
 end
 
 include T
@@ -216,6 +232,31 @@ module Var = struct
     let of_vector = Set.of_vector (module T)
   end
 
+  let demangle =
+    let open Ctypes in
+    let cxa_demangle =
+      (* char *__cxa_demangle(const char *, char *, size_t *, int * ) *)
+      Foreign.foreign "__cxa_demangle"
+        ( string @-> ptr char @-> ptr size_t @-> ptr int
+        @-> returning string_opt )
+    in
+    let null_ptr_char = from_voidp char null in
+    let null_ptr_size_t = from_voidp size_t null in
+    let status = allocate int 0 in
+    fun mangled ->
+      let demangled =
+        cxa_demangle mangled null_ptr_char null_ptr_size_t status
+      in
+      if !@status = 0 then demangled else None
+
+  let pp_demangled fs = function
+    | Var {name} -> (
+      match demangle name with
+      | Some demangled when not (String.equal name demangled) ->
+          Format.fprintf fs "“%s”" demangled
+      | _ -> () )
+    | _ -> ()
+
   let invariant x =
     Invariant.invariant [%here] x [%sexp_of: t]
     @@ fun () -> match x with Var _ -> invariant x | _ -> assert false

sledge/src/llair/exp.mli

@@ -97,6 +97,7 @@ module Var : sig
 
   val equal : t -> t -> bool
   val pp : t pp
+  val pp_demangled : t pp
 
   include Invariant.S with type t := t
 

sledge/src/llair/global.ml

@@ -12,34 +12,13 @@ type t = {var: Var.t; init: Exp.t option; siz: int; typ: Typ.t; loc: Loc.t}
 
 let equal = [%compare.equal: t]
 
-let demangle =
-  let open Ctypes in
-  let cxa_demangle =
-    (* char *__cxa_demangle(const char *, char *, size_t *, int * ) *)
-    Foreign.foreign "__cxa_demangle"
-      ( string @-> ptr char @-> ptr size_t @-> ptr int
-      @-> returning string_opt )
-  in
-  let null_ptr_char = from_voidp char null in
-  let null_ptr_size_t = from_voidp size_t null in
-  let status = allocate int 0 in
-  fun mangled ->
-    let demangled =
-      cxa_demangle mangled null_ptr_char null_ptr_size_t status
-    in
-    if !@status = 0 then demangled else None
-
 let pp fs {var} =
   let name = Var.name var in
   let pf pp =
     Format.pp_open_box fs 2 ;
     Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs pp
   in
-  pf "@%s%t" name (fun fs ->
-      match demangle name with
-      | Some demangled when not (String.equal name demangled) ->
-          Format.fprintf fs "“%s”" demangled
-      | _ -> () )
+  pf "@%s%a" name Var.pp_demangled var
 
 let pp_defn fs {var; init; typ} =
   Format.fprintf fs "@[<2>%a %a%a@]" Typ.pp typ Var.pp var

sledge/src/llair/llair.ml

@@ -282,6 +282,12 @@ module Term = struct
   let return ~exp ~loc = Return {exp; loc} |> check invariant
   let throw ~exc ~loc = Throw {exc; loc} |> check invariant
   let unreachable = Unreachable |> check invariant
+
+  let loc = function
+    | Switch {loc} | Iswitch {loc} | Call {loc} | Return {loc} | Throw {loc}
+      ->
+        loc
+    | Unreachable -> Loc.none
 end
 
 (** Basic-Blocks *)

sledge/src/llair/llair.mli

@@ -168,6 +168,7 @@ module Term : sig
   val return : exp:Exp.t option -> loc:Loc.t -> term
   val throw : exc:Exp.t -> loc:Loc.t -> term
   val unreachable : term
+  val loc : term -> Loc.t
 end
 
 module Block : sig

sledge/src/symbheap/exec.ml

@@ -245,8 +245,9 @@ 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}@;<0 -1>-{%a}@]@]" Sh.pp pre Sh.pp_us xs
-      Sh.pp foot Sh.pp post ;
+    pf "@[%a@]@ @[<2>%a@,@[{%a}@;<0 -1>-{%a}@]@]" Sh.pp pre
+      (Sh.pp_us ~pre:"@<2>∀ ")
+      xs Sh.pp foot Sh.pp post ;
     assert (
       let vs = Set.diff (Set.diff foot.Sh.us xs) pre.Sh.us in
       Set.is_empty vs || Trace.report "unbound foot: {%a}" Var.Set.pp vs ) ;
@@ -274,7 +275,8 @@ let rec exec_specs pre = function
 
 let inst : Sh.t -> Llair.inst -> (Sh.t, _) result =
  fun pre inst ->
-  [%Trace.info "@[<2>exec inst %a from@ %a@]" Llair.Inst.pp inst Sh.pp pre] ;
+  [%Trace.info
+    "@[<2>exec inst %a from@ @[{ %a@ }@]@]" Llair.Inst.pp inst Sh.pp pre] ;
   assert (Set.disjoint (Sh.fv pre) (Llair.Inst.locals inst)) ;
   let us = pre.us in
   ( match inst with

sledge/src/symbheap/sh.ml

@@ -25,22 +25,23 @@ and disjunction = starjunction list
 
 type t = starjunction [@@deriving compare, sexp]
 
-let pp_seg cong fs {loc; bas; len; siz; arr} =
-  let loc = Congruence.normalize cong loc in
-  let bas = Congruence.normalize cong bas in
-  let len = Congruence.normalize cong len in
-  let siz = Congruence.normalize cong siz in
-  let arr = Congruence.normalize cong arr in
-  Format.fprintf fs "@[<2>%a@ @[@[-[ %a, %a )->@]@ %a@]@]" Exp.pp loc Exp.pp
-    bas Exp.pp len Exp.pp (Exp.memory ~siz ~arr)
-
-let pp_us fs us =
+let map_seg {loc; bas; len; siz; arr} ~f =
+  {loc= f loc; bas= f bas; len= f len; siz= f siz; arr= f arr}
+
+let pp_seg fs {loc; bas; len; siz; arr} =
+  Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" Exp.pp loc
+    (fun fs (bas, len) ->
+      if (not (Exp.equal loc bas)) || not (Exp.equal len siz) then
+        Format.fprintf fs " %a, %a " Exp.pp bas Exp.pp len )
+    (bas, len) Exp.pp (Exp.memory ~siz ~arr)
+
+let pp_us ?(pre = ("" : _ fmt)) fs us =
   if not (Set.is_empty us) then
-    Format.fprintf fs "@<2>∀ @[%a@] .@ " Var.Set.pp us
+    [%Trace.fprintf fs "%( %)@[%a@] .@ " pre Var.Set.pp us]
 
 let rec pp_ vs fs {us; xs; cong; pure; heap; djns} =
   Format.pp_open_hvbox fs 0 ;
-  if not (Set.is_empty us) then Format.fprintf fs "@[%a@] .@ " Var.Set.pp us ;
+  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) ;
@@ -61,7 +62,18 @@ let rec pp_ vs fs {us; xs; cong; pure; heap; djns} =
   else
     List.pp
       ~pre:(if first then "  " else "@ @<2>∧ ")
-      "@ * " (pp_seg cong) fs heap ;
+      "@ * " pp_seg fs
+      (List.sort
+         (List.map ~f:(map_seg ~f:(Congruence.normalize cong)) heap)
+         ~compare:(fun s1 s2 ->
+           let b_o = function
+             | Exp.App {op= App {op= Add; arg}; arg= Integer {data}} ->
+                 (arg, data)
+             | e -> (e, Z.zero)
+           in
+           [%compare: Exp.t * (Exp.t * Z.t)]
+             (s1.bas, b_o s1.loc)
+             (s2.bas, b_o s2.loc) )) ;
   List.pp ~pre:"@ * " "@ * "
     (pp_djn (Set.union vs (Set.union us xs)))
     fs djns ;
@@ -77,7 +89,6 @@ and pp_djn vs fs = function
         djn
 
 let pp = pp_ Var.Set.empty
-let pp_seg = pp_seg Congruence.true_
 
 let fold_exps_seg {loc; bas; len; siz; arr} ~init ~f =
   let f b z = Exp.fold_exps b ~init:z ~f in

sledge/src/symbheap/sh.mli

@@ -26,7 +26,7 @@ and disjunction = starjunction list
 type t = starjunction
 
 val pp_seg : seg pp
-val pp_us : Var.Set.t pp
+val pp_us : ?pre:('a, 'a) fmt -> Var.Set.t pp
 val pp : t pp
 
 include Invariant.S with type t := t

sledge/src/trace/trace.ml

@@ -22,7 +22,7 @@ type config = {trace_all: bool; trace_mods_funs: trace_mods_funs}
 let config : config ref =
   ref {trace_all= false; trace_mods_funs= Map.empty (module String)}
 
-let init ?(margin = 160) ~config:c () =
+let init ?(margin = 300) ~config:c () =
   Format.set_margin margin ;
   Format.set_max_indent (margin - 1) ;
   Format.pp_set_margin fs margin ;