[sledge] Add printing of some variables in bold

Summary:
Add a `-color` option to sledge, that prints variable that are
existentially bound as bold.

Reviewed By: ngorogiannis

Differential Revision: D16088750

fbshipit-source-id: bd21cb8a0

sledge/sledge-help.txt

@@ -46,6 +46,7 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s
 === flags ===
 
   [-bound <int>]          stop execution exploration at depth <int>
+  [-colors]               enable printing in colors
   [-function-summaries]   use function summaries (in development)
   [-fuzzer]               add a harness for libFuzzer targets
   [-llair-output <file>]  write generated LLAIR to <file>
@@ -68,6 +69,7 @@ Build a buck target and report the included bitcode files.
 
 === flags ===
 
+  [-colors]          enable printing in colors
   [-margin <cols>]   wrap debug tracing at <cols> columns
   [-modules <file>]  write list of bitcode files to <file>, or to standard
                      output if <file> is `-`
@@ -87,6 +89,7 @@ Link code in a buck target to a single LLVM bitcode module. This also internaliz
 === flags ===
 
   -bitcode-output <file>  write linked bitcode to <file>
+  [-colors]               enable printing in colors
   [-fuzzer]               add a harness for libFuzzer targets
   [-margin <cols>]        wrap debug tracing at <cols> columns
   [-modules <file>]       write list of bitcode files to <file>, or to standard
@@ -122,6 +125,7 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo
 === flags ===
 
   [-bound <int>]          stop execution exploration at depth <int>
+  [-colors]               enable printing in colors
   [-function-summaries]   use function summaries (in development)
   [-fuzzer]               add a harness for libFuzzer targets
   [-llair-output <file>]  write generated LLAIR to <file>
@@ -142,6 +146,7 @@ Translate one or more LLVM bitcode files to LLAIR. Each <input> filename may be
 
 === flags ===
 
+  [-colors]               enable printing in colors
   [-fuzzer]               add a harness for libFuzzer targets
   [-llair-output <file>]  write generated LLAIR to <file>
   [-margin <cols>]        wrap debug tracing at <cols> columns
@@ -161,6 +166,7 @@ The <input> file must be binary LLAIR, such as produced by `sledge translate`.
 === flags ===
 
   [-bound <int>]         stop execution exploration at depth <int>
+  [-colors]              enable printing in colors
   [-function-summaries]  use function summaries (in development)
   [-margin <cols>]       wrap debug tracing at <cols> columns
   [-skip-throw]          do not explore past throwing an exception
@@ -179,6 +185,7 @@ The <input> file must be LLAIR code, as produced by `sledge llvm translate`.
 
 === flags ===
 
+  [-colors]         enable printing in colors
   [-llair <file>]   write generated textual LLAIR to <file>, or to standard
                     output if omitted
   [-margin <cols>]  wrap debug tracing at <cols> columns

sledge/src/control.ml

@@ -280,8 +280,15 @@ let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
 
 let summary_table = Hashtbl.create (module Var)
 
+let pp_st _ =
+  [%Trace.printf
+    "@[<v>%t@]" (fun fs ->
+        Hashtbl.iteri summary_table ~f:(fun ~key ~data ->
+            Format.fprintf fs "@[<v>%a:@ @[%a@]@]@ " Var.pp key
+              (List.pp "@," Domain.pp) data ) )]
+
 let exec_return ~opts stk pre_state (block : Llair.block) exp =
-  [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]
+  [%Trace.call fun {pf} -> pf "from %a@ " Var.pp block.parent.name.var]
   ;
   ( match Stack.pop_return stk with
   | Some (from_call, retn_site, stk) ->
@@ -294,9 +301,10 @@ let exec_return ~opts stk pre_state (block : Llair.block) exp =
         | _ -> violates Llair.Func.invariant block.parent
       in
       let function_summary = exit_state in
-      if opts.function_summaries then
+      if opts.function_summaries then (
         Hashtbl.add_multi summary_table ~key:block.parent.name.var
           ~data:function_summary ;
+        pp_st () ) ;
       let post_state =
         Domain.post block.parent.locals from_call exit_state
       in
@@ -310,11 +318,7 @@ let exec_return ~opts stk pre_state (block : Llair.block) exp =
         | None -> retn_site )
   | None -> Work.skip )
   |>
-  [%Trace.retn fun {pf} _ ->
-    pf "@[<v>%t@]" (fun fs ->
-        Hashtbl.iteri summary_table ~f:(fun ~key ~data ->
-            Format.fprintf fs "@[<v>%a:@ @[%a@]@]@ " Var.pp key
-              (List.pp "@," Domain.pp) data ) )]
+  [%Trace.retn fun {pf} _ -> pf ""]
 
 let exec_throw stk pre_state (block : Llair.block) exc =
   [%Trace.call fun {pf} -> pf "from %a" Var.pp block.parent.name.var]

sledge/src/llair/exp.ml

@@ -242,22 +242,29 @@ let uncurry =
   in
   uncurry_ []
 
-let rec pp fs exp =
+let rec pp ?is_x fs exp =
+  let get_var_style var =
+    match is_x with
+    | None -> `None
+    | Some is_x -> if not (is_x var) then `Bold else `Cyan
+  in
   let pp_ pp fs exp =
     let pf fmt =
       Format.pp_open_box fs 2 ;
       Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
     in
     match exp with
-    | Var {name; id= 0} -> pf "%%%s" name
-    | Var {name; id} -> pf "%%%s_%d" name id
+    | Var {name; id= 0} as var ->
+        Trace.pp_styled (get_var_style var) "%%%s" fs name
+    | Var {name; id} as var ->
+        Trace.pp_styled (get_var_style var) "%%%s_%d" fs name id
     | Nondet {msg} -> pf "nondet \"%s\"" msg
     | Label {name} -> pf "%s" name
     | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null"
     | Splat {byt; siz} -> pf "%a^%a" pp byt pp siz
     | Memory {siz; arr} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr
     | Concat {args} -> pf "%a" (Vector.pp "@,^" pp) args
-    | Integer {data} -> pf "%a" Z.pp data
+    | Integer {data} -> Trace.pp_styled `Magenta "%a" fs Z.pp data
     | Float {data} -> pf "%s" data
     | Eq -> pf "="
     | Dq -> pf "@<1>≠"
@@ -350,7 +357,9 @@ and pp_record fs elts =
 
 type exp = t
 
-let pp_t = pp
+let pp_t = pp ?is_x:None
+let pp_full = pp
+let pp = pp_t
 
 (** Invariant *)
 
@@ -508,7 +517,8 @@ module Var = struct
 
     type t = Set.M(T).t [@@deriving compare, equal, sexp]
 
-    let pp vs = Set.pp pp_t vs
+    let pp_full ?is_x vs = Set.pp (pp_full ?is_x) vs
+    let pp = pp_full ?is_x:None
     let empty = Set.empty (module T)
     let of_list = Set.of_list (module T)
     let of_vector = Set.of_vector (module T)

sledge/src/llair/exp.mli

@@ -81,6 +81,7 @@ val comparator : (t, comparator_witness) Comparator.t
 
 type exp = t
 
+val pp_full : ?is_x:(exp -> bool) -> t pp
 val pp : t pp
 val invariant : ?partial:bool -> t -> unit
 
@@ -95,6 +96,7 @@ module Var : sig
     type t = (var, comparator_witness) Set.t
     [@@deriving compare, equal, sexp]
 
+    val pp_full : ?is_x:(exp -> bool) -> t pp
     val pp : t pp
     val empty : t
     val of_list : var list -> t

sledge/src/sledge.ml

@@ -31,8 +31,8 @@ let command ~summary ?readme param =
     and margin =
       flag "margin" ~doc:"<cols> wrap debug tracing at <cols> columns"
         (optional int)
-    in
-    Trace.init ?margin ~config ()
+    and colors = flag "colors" no_arg ~doc:"enable printing in colors" in
+    Trace.init ~colors ?margin ~config ()
   in
   let wrap main () =
     try

sledge/src/symbheap/equality.ml

@@ -41,10 +41,11 @@ let pp fs {sat; rep} =
     (pp_alist Exp.pp pp_exp_v)
     (Map.to_alist rep)
 
-let pp_classes fs r =
+let pp_classes ?is_x fs r =
   List.pp "@ @<2>∧ "
     (fun fs (key, data) ->
-      Format.fprintf fs "@[%a@ = %a@]" Exp.pp key (List.pp "@ = " Exp.pp)
+      Format.fprintf fs "@[%a@ = %a@]" (Exp.pp_full ?is_x) key
+        (List.pp "@ = " (Exp.pp_full ?is_x))
         (List.sort ~compare:Exp.compare data) )
     fs
     (Map.to_alist (classes r))

sledge/src/symbheap/equality.mli

@@ -11,7 +11,7 @@
 type t [@@deriving compare, equal, sexp]
 
 val pp : t pp
-val pp_classes : t pp
+val pp_classes : ?is_x:(Exp.t -> bool) -> t pp
 
 include Invariant.S with type t := t
 

sledge/src/symbheap/sh.ml

@@ -28,12 +28,13 @@ type t = starjunction [@@deriving compare, equal, sexp]
 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
+let pp_seg ?is_x fs {loc; bas; len; siz; arr} =
+  let exp_pp = Exp.pp_full ?is_x in
+  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)
+        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))
@@ -42,18 +43,20 @@ 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 all_xs fs {us; xs; cong; pure; heap; djns} =
   Format.pp_open_hvbox fs 0 ;
+  let all_xs = Set.union all_xs xs in
+  let is_x var = Set.mem all_xs (Option.value_exn (Var.of_exp var)) in
   pp_us fs us ;
   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 ;
+    Format.fprintf fs "@<2>∃ @[%a@] ." (Var.Set.pp_full ~is_x) 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 ;
+    Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.pp_full ~is_x) xs_d_vs ;
   let first = Equality.is_true cong in
   if not first then Format.fprintf fs "  " ;
-  Equality.pp_classes fs cong ;
+  Equality.pp_classes ~is_x fs cong ;
   let pure_exps =
     List.filter_map pure ~f:(fun e ->
         let e' = Equality.normalize cong e in
@@ -61,7 +64,7 @@ let rec pp vs fs {us; xs; cong; pure; heap; djns} =
   in
   List.pp
     ~pre:(if first then "  " else "@ @<2>∧ ")
-    "@ @<2>∧ " Exp.pp fs pure_exps ;
+    "@ @<2>∧ " (Exp.pp_full ~is_x) fs pure_exps ;
   let first = first && List.is_empty pure_exps in
   if List.is_empty heap then
     Format.fprintf fs
@@ -70,7 +73,7 @@ let rec pp vs fs {us; xs; cong; pure; heap; djns} =
   else
     List.pp
       ~pre:(if first then "  " else "@ @<2>∧ ")
-      "@ * " pp_seg fs
+      "@ * " (pp_seg ~is_x) fs
       (List.sort
          (List.map ~f:(map_seg ~f:(Equality.normalize cong)) heap)
          ~compare:(fun s1 s2 ->
@@ -86,21 +89,21 @@ let rec pp vs fs {us; xs; cong; pure; heap; djns} =
   List.pp
     ~pre:(if first then "  " else "@ * ")
     "@ * "
-    (pp_djn (Set.union vs (Set.union us xs)))
+    (pp_djn (Set.union vs (Set.union us xs)) all_xs)
     fs djns ;
   Format.pp_close_box fs ()
 
-and pp_djn vs fs = function
+and pp_djn vs all_xs fs = function
   | [] -> Format.fprintf fs "false"
   | djn ->
       Format.fprintf fs "@[<hv>( %a@ )@]"
         (List.pp "@ @<2>∨ " (fun fs sjn ->
-             Format.fprintf fs "@[<hv 1>(%a)@]" (pp vs)
+             Format.fprintf fs "@[<hv 1>(%a)@]" (pp vs all_xs)
                {sjn with us= Set.diff sjn.us vs} ))
         djn
 
-let pp = pp Var.Set.empty
-let pp_djn = pp_djn Var.Set.empty
+let pp = pp Var.Set.empty Var.Set.empty
+let pp_djn = pp_djn Var.Set.empty 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

sledge/src/symbheap/sh.mli

@@ -25,7 +25,7 @@ and disjunction = starjunction list
 
 type t = starjunction [@@deriving equal, compare, sexp]
 
-val pp_seg : seg pp
+val pp_seg : ?is_x:(Exp.t -> bool) -> 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

sledge/src/trace/trace.ml

@@ -17,9 +17,15 @@ type trace_mod_funs =
   {trace_mod: bool option; trace_funs: bool Map.M(String).t}
 
 type trace_mods_funs = trace_mod_funs Map.M(String).t
-type config = {trace_all: bool; trace_mods_funs: trace_mods_funs}
 
-let none = {trace_all= false; trace_mods_funs= Map.empty (module String)}
+type config =
+  {trace_all: bool; trace_mods_funs: trace_mods_funs; colors: bool}
+
+let none =
+  { trace_all= false
+  ; trace_mods_funs= Map.empty (module String)
+  ; colors= false }
+
 let all = {none with trace_all= true}
 let config : config ref = ref none
 
@@ -77,14 +83,30 @@ let parse s =
       Ok {none with trace_mods_funs}
   with Assert_failure _ as exn -> Error exn
 
-let init ?(margin = 240) ~config:c () =
+let pp_styled style fmt fs =
+  Format.pp_open_box fs 2 ;
+  if (not !config.colors) || match style with `None -> true | _ -> false
+  then Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
+  else (
+    ( match style with
+    | `Bold -> Format.fprintf fs "\027[1m"
+    | `Cyan -> Format.fprintf fs "\027[36m"
+    | `Magenta -> Format.fprintf fs "\027[95m"
+    | _ -> () ) ;
+    Format.kfprintf
+      (fun fs ->
+        Format.fprintf fs "\027[0m" ;
+        Format.pp_close_box fs () )
+      fs fmt )
+
+let init ?(colors = false) ?(margin = 240) ~config:c () =
   Format.set_margin margin ;
   Format.set_max_indent (margin - 1) ;
   Format.pp_set_margin fs margin ;
   Format.pp_set_max_indent fs (margin - 1) ;
   Format.pp_open_vbox fs 0 ;
   Caml.at_exit flush ;
-  config := c
+  config := {c with colors}
 
 let unwrap s =
   let rec index s i =

sledge/src/trace/trace.mli

@@ -19,18 +19,26 @@ type trace_mods_funs = trace_mod_funs Map.M(String).t
 type config =
   { trace_all: bool  (** Enable all tracing *)
   ; trace_mods_funs: trace_mods_funs
-        (** Specify tracing of individual toplevel modules *) }
+        (** Specify tracing of individual toplevel modules *)
+  ; colors: bool  (** Enable color output *) }
 
 val none : config
 val all : config
 val parse : string -> (config, exn) result
 
-val init : ?margin:int -> config:config -> unit -> unit
+val init : ?colors:bool -> ?margin:int -> config:config -> unit -> unit
 (** Initialize the configuration of debug tracing. *)
 
 type 'a printf = ('a, Formatter.t, unit) format -> 'a
 type pf = {pf: 'a. 'a printf}
 
+val pp_styled :
+     [> `Bold | `Cyan | `Magenta | `None]
+  -> ('a, Format.formatter, unit, unit) format4
+  -> Format.formatter
+  -> 'a
+(** If config.colors is set to true, print in the specificed color *)
+
 val printf : string -> string -> 'a printf
 (** Like [Format.printf], if enabled, otherwise like [Format.iprintf]. *)