From b5b8259ea7f90588afc85a04a94e402c5bc68e47 Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Tue, 9 Jul 2019 03:14:14 -0700 Subject: [PATCH] [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 | 7 +++++++ sledge/src/control.ml | 18 ++++++++++------- sledge/src/llair/exp.ml | 22 +++++++++++++++------ sledge/src/llair/exp.mli | 2 ++ sledge/src/sledge.ml | 4 ++-- sledge/src/symbheap/equality.ml | 5 +++-- sledge/src/symbheap/equality.mli | 2 +- sledge/src/symbheap/sh.ml | 33 +++++++++++++++++--------------- sledge/src/symbheap/sh.mli | 2 +- sledge/src/trace/trace.ml | 30 +++++++++++++++++++++++++---- sledge/src/trace/trace.mli | 12 ++++++++++-- 11 files changed, 97 insertions(+), 40 deletions(-) diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 3d4b2473a..a8df5a6e1 100644 --- a/sledge/sledge-help.txt +++ b/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 ] stop execution exploration at depth + [-colors] enable printing in colors [-function-summaries] use function summaries (in development) [-fuzzer] add a harness for libFuzzer targets [-llair-output ] write generated LLAIR to @@ -68,6 +69,7 @@ Build a buck target and report the included bitcode files. === flags === + [-colors] enable printing in colors [-margin ] wrap debug tracing at columns [-modules ] write list of bitcode files to , or to standard output if is `-` @@ -87,6 +89,7 @@ Link code in a buck target to a single LLVM bitcode module. This also internaliz === flags === -bitcode-output write linked bitcode to + [-colors] enable printing in colors [-fuzzer] add a harness for libFuzzer targets [-margin ] wrap debug tracing at columns [-modules ] write list of bitcode files to , or to standard @@ -122,6 +125,7 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo === flags === [-bound ] stop execution exploration at depth + [-colors] enable printing in colors [-function-summaries] use function summaries (in development) [-fuzzer] add a harness for libFuzzer targets [-llair-output ] write generated LLAIR to @@ -142,6 +146,7 @@ Translate one or more LLVM bitcode files to LLAIR. Each filename may be === flags === + [-colors] enable printing in colors [-fuzzer] add a harness for libFuzzer targets [-llair-output ] write generated LLAIR to [-margin ] wrap debug tracing at columns @@ -161,6 +166,7 @@ The file must be binary LLAIR, such as produced by `sledge translate`. === flags === [-bound ] stop execution exploration at depth + [-colors] enable printing in colors [-function-summaries] use function summaries (in development) [-margin ] wrap debug tracing at columns [-skip-throw] do not explore past throwing an exception @@ -179,6 +185,7 @@ The file must be LLAIR code, as produced by `sledge llvm translate`. === flags === + [-colors] enable printing in colors [-llair ] write generated textual LLAIR to , or to standard output if omitted [-margin ] wrap debug tracing at columns diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 845c01892..10e60b003 100644 --- a/sledge/src/control.ml +++ b/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 + "@[%t@]" (fun fs -> + Hashtbl.iteri summary_table ~f:(fun ~key ~data -> + Format.fprintf fs "@[%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 "@[%t@]" (fun fs -> - Hashtbl.iteri summary_table ~f:(fun ~key ~data -> - Format.fprintf fs "@[%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] diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index cd0e7d896..261baff1d 100644 --- a/sledge/src/llair/exp.ml +++ b/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) diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index 45c75d209..416e23c2c 100644 --- a/sledge/src/llair/exp.mli +++ b/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 diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml index 029580f2d..f381b1bed 100644 --- a/sledge/src/sledge.ml +++ b/sledge/src/sledge.ml @@ -31,8 +31,8 @@ let command ~summary ?readme param = and margin = flag "margin" ~doc:" wrap debug tracing at 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 diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml index 6a00729fe..36d920e47 100644 --- a/sledge/src/symbheap/equality.ml +++ b/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)) diff --git a/sledge/src/symbheap/equality.mli b/sledge/src/symbheap/equality.mli index cf80ea97b..52d236d72 100644 --- a/sledge/src/symbheap/equality.mli +++ b/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 diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 010c224e8..3f8ce82a4 100644 --- a/sledge/src/symbheap/sh.ml +++ b/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 "@[( %a@ )@]" (List.pp "@ @<2>∨ " (fun fs sjn -> - Format.fprintf fs "@[(%a)@]" (pp vs) + Format.fprintf fs "@[(%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 diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli index 4a64cdcae..94198f72f 100644 --- a/sledge/src/symbheap/sh.mli +++ b/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 diff --git a/sledge/src/trace/trace.ml b/sledge/src/trace/trace.ml index 0130df972..4a5aff80f 100644 --- a/sledge/src/trace/trace.ml +++ b/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 = diff --git a/sledge/src/trace/trace.mli b/sledge/src/trace/trace.mli index 3016f1f91..65ea99d13 100644 --- a/sledge/src/trace/trace.mli +++ b/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]. *)