From 334661b47406cb25a050011c4fc3f4e309dbb830 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 4 Sep 2020 13:38:17 -0700 Subject: [PATCH] [sledge] Improve: result status reporting and unhandled exceptions Summary: Add a Report.status type to represent the overall status of an analysis run, and revise handling of backtraces to preserve the trace of the originally-raised exception in more cases. Reviewed By: ngorogiannis Differential Revision: D23459518 fbshipit-source-id: a99fe0d14 --- sledge/bin/sledge_buck.ml | 6 +-- sledge/bin/sledge_buck.mli | 4 +- sledge/bin/sledge_cli.ml | 73 ++++++++++++++++------------- sledge/bin/smtlib.ml | 7 ++- sledge/bin/smtlib.mli | 5 +- sledge/dune | 2 +- sledge/nonstdlib/NS.ml | 47 +++++++++++++++---- sledge/nonstdlib/NS.mli | 9 +++- sledge/sledge-help.txt | 25 ++++++++++ sledge/sledge.opam | 1 + sledge/src/fol.ml | 6 ++- sledge/src/report.ml | 96 ++++++++++++++++++++++++++++++++++++-- sledge/src/report.mli | 32 ++++++++++++- 13 files changed, 253 insertions(+), 60 deletions(-) diff --git a/sledge/bin/sledge_buck.ml b/sledge/bin/sledge_buck.ml index c019c70bf..805b241b0 100644 --- a/sledge/bin/sledge_buck.ml +++ b/sledge/bin/sledge_buck.ml @@ -190,7 +190,7 @@ let ( |**> ) = Command.Param.map2 ~f:(fun a f b -> f b a) let abs_path_arg = Command.Param.(Arg_type.map string ~f:(make_absolute cwd)) -let main ~(command : unit Command.basic_command) ~analyze = +let main ~(command : Report.status Command.basic_command) ~analyze = let bitcode_inputs = let%map_open target = anon ("" %: string) and modules = @@ -214,7 +214,7 @@ let main ~(command : unit Command.basic_command) ~analyze = let readme () = "Build a buck target and report the included bitcode files." in - let param = bitcode_inputs >>| fun _ () -> () in + let param = bitcode_inputs >>| fun _ () -> Report.Ok in command ~summary ~readme param in let analyze_cmd = @@ -242,7 +242,7 @@ let main ~(command : unit Command.basic_command) ~analyze = in fun () -> llvm_link_opt ~fuzzer ~bitcode_output in - let param = bitcode_inputs |**> link in + let param = bitcode_inputs |**> link >>| fun _ () -> Report.Ok in command ~summary ~readme param in let summary = "integration with Buck" in diff --git a/sledge/bin/sledge_buck.mli b/sledge/bin/sledge_buck.mli index 57de68f51..1419d20dd 100644 --- a/sledge/bin/sledge_buck.mli +++ b/sledge/bin/sledge_buck.mli @@ -6,6 +6,6 @@ *) val main : - command:unit Command.basic_command - -> analyze:(string list -> unit -> unit) Command.Param.t + command:Report.status Command.basic_command + -> analyze:(string list -> unit -> Report.status) Command.Param.t -> Command.t diff --git a/sledge/bin/sledge_cli.ml b/sledge/bin/sledge_cli.ml index c68a71aec..b730460bb 100644 --- a/sledge/bin/sledge_cli.ml +++ b/sledge/bin/sledge_cli.ml @@ -33,40 +33,45 @@ let command ~summary ?readme param = flag "trace" ~doc:" enable debug tracing" (optional_with_default Trace.none (Arg_type.create (fun s -> Trace.parse s |> Result.ok_exn))) + and colors = flag "colors" no_arg ~doc:"enable printing in colors" and margin = flag "margin" ~doc:" wrap debug tracing at columns" (optional int) - and colors = flag "colors" no_arg ~doc:"enable printing in colors" in - Trace.init ~colors ?margin ~config () + and report = + flag "report" (optional string) + ~doc: + " write report sexp to , or to standard error if \ + \"-\"" + and append_report = + flag "append-report" no_arg ~doc:"append to report file" + in + Trace.init ~colors ?margin ~config () ; + Option.iter ~f:(Report.init ~append:append_report) report in - let wrap main () = - try - main () |> ignore ; - Trace.flush () ; - Format.printf "@\nRESULT: Success: Invalid Accesses: %i@." - (Report.invalid_access_count ()) - with - | Smtlib.Unsound -> - Trace.flush () ; - Format.printf "@\nRESULT: Unsound@." - | Smtlib.Incomplete -> - Trace.flush () ; - Format.printf "@\nRESULT: Incomplete@." - | exn -> - let bt = Printexc.get_raw_backtrace () in - Trace.flush () ; - ( match exn with - | Frontend.Invalid_llvm msg -> - Format.printf "@\nRESULT: Invalid input: %s@." msg - | Unimplemented msg -> - Format.printf "@\nRESULT: Unimplemented: %s@." msg - | Failure msg -> Format.printf "@\nRESULT: Internal error: %s@." msg - | _ -> - Format.printf "@\nRESULT: Unknown error: %s@." - (Printexc.to_string exn) ) ; - Printexc.raise_with_backtrace exn bt + let flush main () = Fun.protect main ~finally:Trace.flush in + let report main () = + try main () |> Report.status + with exn -> + let bt = + match exn with + | Invariant.Violation (_, bt, _, _) -> bt + | Replay (_, bt, _) -> bt + | _ -> Printexc.get_raw_backtrace () + in + let rec status_of_exn = function + | Invariant.Violation (exn, _, _, _) | Replay (exn, _, _) -> + status_of_exn exn + | Frontend.Invalid_llvm msg -> Report.InvalidInput msg + | Unimplemented msg -> Report.Unimplemented msg + | Assert_failure _ as exn -> + Report.InternalError (Sexp.to_string_hum (sexp_of_exn exn)) + | Failure msg -> Report.InternalError msg + | exn -> Report.UnknownError (Printexc.to_string exn) + in + Report.status (status_of_exn exn) ; + Printexc.raise_with_backtrace exn bt in - Command.basic ~summary ?readme (trace *> param >>| wrap) + Command.basic ~summary ?readme (trace *> param >>| flush >>| report) let marshal program file = Out_channel.with_file file ~f:(fun oc -> Marshal.to_channel oc program []) @@ -133,7 +138,8 @@ let analyze = let skip_throw = not exceptions in Domain_sh.simplify_states := not no_simplify_states ; Timer.enabled := stats ; - exec {bound; skip_throw; function_summaries; entry_points; globals} pgm + exec {bound; skip_throw; function_summaries; entry_points; globals} pgm ; + Report.safe_or_unsafe () let analyze_cmd = let summary = "analyze LLAIR code" in @@ -155,12 +161,13 @@ let disassemble = in fun program () -> let pgm = program () in - match llair_txt_output with + ( match llair_txt_output with | None -> Format.printf "%a@." Llair.Program.pp pgm | Some file -> Out_channel.with_file file ~f:(fun oc -> let fs = Format.formatter_of_out_channel oc in - Format.fprintf fs "%a@." Llair.Program.pp pgm ) + Format.fprintf fs "%a@." Llair.Program.pp pgm ) ) ; + Report.Ok let disassemble_cmd = let summary = "print LLAIR code in textual form" in @@ -219,7 +226,7 @@ let llvm_grp = textual (.ll) form; or of the form @, where \ names a file containing one per line." in - let param = translate_inputs in + let param = translate_inputs >>| fun _ () -> Report.Ok in command ~summary ~readme param in let disassemble_cmd = diff --git a/sledge/bin/smtlib.ml b/sledge/bin/smtlib.ml index 60c7fa17b..f8c80daed 100644 --- a/sledge/bin/smtlib.ml +++ b/sledge/bin/smtlib.ml @@ -183,4 +183,9 @@ let process_stmt (stmt : Smt.Ast.statement) = | Stmt_exit -> () let process filename = - List.iter ~f:process_stmt (Smt.parse_file_exn filename) + try + List.iter ~f:process_stmt (Smt.parse_file_exn filename) ; + Report.Ok + with + | Unsound -> Report.Unsound + | Incomplete -> Report.Incomplete diff --git a/sledge/bin/smtlib.mli b/sledge/bin/smtlib.mli index f80ee12ee..edd0612fc 100644 --- a/sledge/bin/smtlib.mli +++ b/sledge/bin/smtlib.mli @@ -7,7 +7,4 @@ (** Process SMT-LIB benchmarks using SLEdge's first-order theory solver. *) -exception Unsound -exception Incomplete - -val process : string -> unit +val process : string -> Report.status diff --git a/sledge/dune b/sledge/dune index f7a2ffa5c..72eacd7fe 100644 --- a/sledge/dune +++ b/sledge/dune @@ -62,7 +62,7 @@ (library (name sledge) (public_name sledge) - (libraries nonstdlib llair ses) + (libraries mtime mtime.clock.os nonstdlib llair ses) (flags (:standard -open NS)) (preprocess diff --git a/sledge/nonstdlib/NS.ml b/sledge/nonstdlib/NS.ml index 91aeba220..039efde7a 100644 --- a/sledge/nonstdlib/NS.ml +++ b/sledge/nonstdlib/NS.ml @@ -12,6 +12,21 @@ module Monad = Monad (** Failures *) +exception Replay of exn * Printexc.raw_backtrace * Sexp.t + +let register_sexp_of_exn exn sexp_of_exn = + Sexplib.Conv.Exn_converter.add + (Obj.Extension_constructor.of_val exn) + sexp_of_exn + +;; +register_sexp_of_exn + (Replay (Stdlib.Not_found, Printexc.get_callstack 1, Sexp.List [])) + (function + | Replay (exn, _, payload) -> + Sexp.List [Atom "Replay"; sexp_of_exn exn; payload] + | exn -> Sexp.Atom (Printexc.to_string exn) ) + let fail = Trace.fail exception Unimplemented of string @@ -55,20 +70,32 @@ let violates f x = module Invariant = struct include Core.Invariant + exception + Violation of + exn * Printexc.raw_backtrace * Source_code_position.t * Sexp.t + + ;; + register_sexp_of_exn + (Violation + ( Stdlib.Not_found + , Printexc.get_callstack 1 + , Lexing.dummy_pos + , Sexp.List [] )) + (function + | Violation (exn, _, pos, payload) -> + Sexp.List + [ Atom "Invariant.Violation" + ; sexp_of_exn exn + ; Source_code_position.sexp_of_t pos + ; payload ] + | exn -> Sexp.Atom (Printexc.to_string exn) ) + let invariant here t sexp_of_t f = assert ( ( try f () - with exn -> + with exn0 -> let bt = Printexc.get_raw_backtrace () in - let exn = - Error.to_exn - (Error.create_s - (Sexp.List - [ Atom "invariant failed" - ; sexp_of_exn exn - ; Source_code_position.sexp_of_t here - ; sexp_of_t t ])) - in + let exn = Violation (exn0, bt, here, sexp_of_t t) in Printexc.raise_with_backtrace exn bt ) ; true ) end diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli index 876217f0c..aefaa5b9a 100644 --- a/sledge/nonstdlib/NS.mli +++ b/sledge/nonstdlib/NS.mli @@ -38,6 +38,7 @@ val ( <$ ) : ('a -> unit) -> 'a -> 'a (** Failures *) +exception Replay of exn * Printexc.raw_backtrace * Sexp.t exception Unimplemented of string val fail : ('a, unit -> _) fmt -> 'a @@ -68,7 +69,13 @@ val violates : ('a -> unit) -> 'a -> _ (** Extensions *) -module Invariant : module type of Core.Invariant +module Invariant : sig + include module type of Core.Invariant + + exception + Violation of + exn * Printexc.raw_backtrace * Source_code_position.t * Sexp.t +end (** Containers *) diff --git a/sledge/sledge-help.txt b/sledge/sledge-help.txt index 55186c09f..67eb9dfdc 100644 --- a/sledge/sledge-help.txt +++ b/sledge/sledge-help.txt @@ -47,6 +47,7 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s === flags === + [-append-report] append to report file [-bound ] stop execution exploration at depth [-colors] enable printing in colors [-domain ] select abstract domain; must be one of "sh" (default, @@ -65,6 +66,8 @@ Analyze code in a buck target. This is a convenience wrapper for the sequence `s libraries [-no-simplify-states] do not simplify states during symbolic execution [-preanalyze-globals] pre-analyze global variables used by each function + [-report ] write report sexp to , or to standard error if + "-" [-stats] output performance statistics to stderr [-trace ] enable debug tracing [-help] print this help text and exit @@ -81,10 +84,12 @@ Build a buck target and report the included bitcode files. === flags === + [-append-report] append to report file [-colors] enable printing in colors [-margin ] wrap debug tracing at columns [-modules ] write list of bitcode files to , or to standard output if is `-` + [-report ] write report sexp to , or to standard error if "-" [-trace ] enable debug tracing [-help] print this help text and exit (alias: -?) @@ -101,11 +106,14 @@ Link code in a buck target to a single LLVM bitcode module. This also internaliz === flags === -bitcode-output write linked bitcode to + [-append-report] append to report file [-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 output if is `-` + [-report ] write report sexp to , or to standard error if + "-" [-trace ] enable debug tracing [-help] print this help text and exit (alias: -?) @@ -137,6 +145,7 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo === flags === + [-append-report] append to report file [-bound ] stop execution exploration at depth [-colors] enable printing in colors [-domain ] select abstract domain; must be one of "sh" (default, @@ -153,6 +162,8 @@ Analyze code in one or more LLVM bitcode files. This is a convenience wrapper fo libraries [-no-simplify-states] do not simplify states during symbolic execution [-preanalyze-globals] pre-analyze global variables used by each function + [-report ] write report sexp to , or to standard error if + "-" [-stats] output performance statistics to stderr [-trace ] enable debug tracing [-help] print this help text and exit @@ -169,6 +180,7 @@ Translate one or more LLVM bitcode files to LLAIR. Each filename may be === flags === + [-append-report] append to report file [-colors] enable printing in colors [-fuzzer] add a harness for libFuzzer targets [-llair-output ] write generated LLAIR to @@ -177,6 +189,8 @@ Translate one or more LLVM bitcode files to LLAIR. Each filename may be points specified in the config file [-no-models] do not add models for C/C++ runtime and standard libraries + [-report ] write report sexp to , or to standard error if + "-" [-trace ] enable debug tracing [-help] print this help text and exit (alias: -?) @@ -192,6 +206,7 @@ The file must be LLVM bitcode. === flags === + [-append-report] append to report file [-colors] enable printing in colors [-fuzzer] add a harness for libFuzzer targets [-llair-output ] write generated LLAIR to @@ -202,6 +217,8 @@ The file must be LLVM bitcode. points specified in the config file [-no-models] do not add models for C/C++ runtime and standard libraries + [-report ] write report sexp to , or to standard error + if "-" [-trace ] enable debug tracing [-help] print this help text and exit (alias: -?) @@ -217,6 +234,7 @@ The file must be binary LLAIR, such as produced by `sledge translate`. === flags === + [-append-report] append to report file [-bound ] stop execution exploration at depth [-colors] enable printing in colors [-domain ] select abstract domain; must be one of "sh" (default, @@ -227,6 +245,8 @@ The file must be binary LLAIR, such as produced by `sledge translate`. [-margin ] wrap debug tracing at columns [-no-simplify-states] do not simplify states during symbolic execution [-preanalyze-globals] pre-analyze global variables used by each function + [-report ] write report sexp to , or to standard error if + "-" [-stats] output performance statistics to stderr [-trace ] enable debug tracing [-help] print this help text and exit @@ -243,10 +263,13 @@ The file must be LLAIR code, as produced by `sledge llvm translate`. === flags === + [-append-report] append to report file [-colors] enable printing in colors [-llair-txt-output ] write generated textual LLAIR to , or to standard output if omitted [-margin ] wrap debug tracing at columns + [-report ] write report sexp to , or to standard error + if "-" [-trace ] enable debug tracing [-help] print this help text and exit (alias: -?) @@ -262,8 +285,10 @@ The file is interpreted as an SMT-LIB 2 benchmark. === flags === + [-append-report] append to report file [-colors] enable printing in colors [-margin ] wrap debug tracing at columns + [-report ] write report sexp to , or to standard error if "-" [-trace ] enable debug tracing [-help] print this help text and exit (alias: -?) diff --git a/sledge/sledge.opam b/sledge/sledge.opam index fb6ad21d0..9a1d04b12 100644 --- a/sledge/sledge.opam +++ b/sledge/sledge.opam @@ -21,6 +21,7 @@ depends: [ "fpath" "iter" "llvm" {= "8.0.0"} + "mtime" "ppx_compare" "ppx_hash" "shexp" diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 784bec2db..969c6b575 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -1652,7 +1652,11 @@ module Context = struct in if not [%debug] then f () else - try f () with exn -> raise_s ([%sexp_of: exn * call] (exn, call ())) + try f () + with exn -> + let bt = Printexc.get_raw_backtrace () in + let sexp = sexp_of_call (call ()) in + raise (Replay (exn, bt, sexp)) let add_tmr = Timer.create "add" ~at_exit:report let union_tmr = Timer.create "union" ~at_exit:report diff --git a/sledge/src/report.ml b/sledge/src/report.ml index 2555ca8ce..e9a118640 100644 --- a/sledge/src/report.ml +++ b/sledge/src/report.ml @@ -22,11 +22,10 @@ let unknown_call call = | _ -> () ) call Llair.Term.pp call] -let count = ref 0 -let invalid_access_count () = !count +let invalid_access_count = ref 0 let invalid_access fmt_thunk pp access loc = - Int.incr count ; + Int.incr invalid_access_count ; let rep fs = Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Llair.Loc.pp (loc access) pp access @@ -40,3 +39,94 @@ let invalid_access_inst fmt_thunk inst = let invalid_access_term fmt_thunk term = invalid_access fmt_thunk Llair.Term.pp term Llair.Term.loc + +type status = + | Safe + | Unsafe of int + | Ok + | Unsound + | Incomplete + | InvalidInput of string + | Unimplemented of string + | InternalError of string + | Timeout + | Memout + | Crash of string + | UnknownError of string +[@@deriving compare, equal, sexp] + +let pp_status ppf stat = + let pf fmt = Format.fprintf ppf fmt in + match stat with + | Safe -> pf "Safe" + | Unsafe i -> pf "Unsafe: %i" i + | Ok -> pf "Ok" + | Unsound -> pf "Unsound" + | Incomplete -> pf "Incomplete" + | InvalidInput msg -> pf "Invalid input: %s" msg + | Unimplemented msg -> pf "Unimpemented: %s" msg + | InternalError msg -> pf "Internal error: %s" msg + | Timeout -> pf "Timeout" + | Memout -> pf "Memout" + | Crash msg -> pf "Crash: %s" msg + | UnknownError msg -> pf "Unknown error: %s" msg + +let safe_or_unsafe () = + if !invalid_access_count = 0 then Safe else Unsafe !invalid_access_count + +type gc_stats = {allocated: float; promoted: float; peak_size: float} +[@@deriving sexp] + +type entry = + | ProcessTimes of float * Unix.process_times + | GcStats of gc_stats + | Status of status +[@@deriving sexp] + +let process_times () = + let ptimes = Unix.times () in + let etime = + try Mtime.Span.to_s (Mtime_clock.elapsed ()) with Sys_error _ -> 0. + in + ProcessTimes (etime, ptimes) + +let gc_stats () = + let words_to_MB n = n /. float (Sys.word_size / 8) /. (1024. *. 1024.) in + let ctrl = Gc.get () in + let stat = Gc.quick_stat () in + let allocated = + words_to_MB (stat.minor_words +. stat.major_words -. stat.promoted_words) + in + let promoted = words_to_MB stat.promoted_words in + let peak_size = + words_to_MB (float (ctrl.minor_heap_size + stat.top_heap_words)) + in + GcStats {allocated; promoted; peak_size} + +type t = {name: string; entry: entry} [@@deriving sexp] + +let chan = ref None +let name = ref "" + +let output entry = + Option.iter !chan ~f:(fun chan -> + Out_channel.output_string chan + (Sexp.to_string (sexp_of_t {name= !name; entry})) ; + Out_channel.newline chan ) + +let init ?append filename = + (chan := + match filename with + | "" -> None + | "-" -> Some Out_channel.stderr + | _ -> Some (Out_channel.create ?append filename)) ; + name := + Option.value + (Stdlib.Filename.chop_suffix_opt ~suffix:".sexp" filename) + ~default:filename ; + at_exit (fun () -> + output (process_times ()) ; + output (gc_stats ()) ; + Option.iter ~f:Out_channel.close_no_err !chan ) + +let status s = output (Status s) diff --git a/sledge/src/report.mli b/sledge/src/report.mli index 941b268c6..8d2b50f31 100644 --- a/sledge/src/report.mli +++ b/sledge/src/report.mli @@ -7,7 +7,37 @@ (** Issue reporting *) +val init : ?append:bool -> string -> unit val unknown_call : Llair.term -> unit val invalid_access_inst : (Formatter.t -> unit) -> Llair.inst -> unit val invalid_access_term : (Formatter.t -> unit) -> Llair.term -> unit -val invalid_access_count : unit -> int + +type status = + | Safe + | Unsafe of int + | Ok + | Unsound + | Incomplete + | InvalidInput of string + | Unimplemented of string + | InternalError of string + | Timeout + | Memout + | Crash of string + | UnknownError of string +[@@deriving compare, equal, sexp] + +val pp_status : status pp +val safe_or_unsafe : unit -> status +val status : status -> unit + +type gc_stats = {allocated: float; promoted: float; peak_size: float} +[@@deriving sexp] + +type entry = + | ProcessTimes of float * Unix.process_times + | GcStats of gc_stats + | Status of status +[@@deriving sexp] + +type t = {name: string; entry: entry} [@@deriving sexp]