[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

@@ -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 ("<target>" %: 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

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

sledge/bin/sledge_cli.ml

@@ -33,40 +33,45 @@ let command ~summary ?readme param =
       flag "trace" ~doc:"<spec> 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:"<cols> wrap debug tracing at <cols> 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:
+          "<file> write report sexp to <file>, 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 @<argsfile>, where <argsfile> \
        names a file containing one <input> per line."
     in
-    let param = translate_inputs in
+    let param = translate_inputs >>| fun _ () -> Report.Ok in
     command ~summary ~readme param
   in
   let disassemble_cmd =

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

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

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

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

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 *)
 

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 <int>]          stop execution exploration at depth <int>
   [-colors]               enable printing in colors
   [-domain <string>]      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 <file>]        write report sexp to <file>, or to standard error if
+                          "-"
   [-stats]                output performance statistics to stderr
   [-trace <spec>]         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 <cols>]   wrap debug tracing at <cols> columns
   [-modules <file>]  write list of bitcode files to <file>, or to standard
                      output if <file> is `-`
+  [-report <file>]   write report sexp to <file>, or to standard error if "-"
   [-trace <spec>]    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 <file>  write linked bitcode to <file>
+  [-append-report]        append to report 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
                           output if <file> is `-`
+  [-report <file>]        write report sexp to <file>, or to standard error if
+                          "-"
   [-trace <spec>]         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 <int>]          stop execution exploration at depth <int>
   [-colors]               enable printing in colors
   [-domain <string>]      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 <file>]        write report sexp to <file>, or to standard error if
+                          "-"
   [-stats]                output performance statistics to stderr
   [-trace <spec>]         enable debug tracing
   [-help]                 print this help text and exit
@@ -169,6 +180,7 @@ Translate one or more LLVM bitcode files to LLAIR. Each <input> filename may be
 
 === flags ===
 
+  [-append-report]        append to report file
   [-colors]               enable printing in colors
   [-fuzzer]               add a harness for libFuzzer targets
   [-llair-output <file>]  write generated LLAIR to <file>
@@ -177,6 +189,8 @@ Translate one or more LLVM bitcode files to LLAIR. Each <input> filename may be
                           points specified in the config file
   [-no-models]            do not add models for C/C++ runtime and standard
                           libraries
+  [-report <file>]        write report sexp to <file>, or to standard error if
+                          "-"
   [-trace <spec>]         enable debug tracing
   [-help]                 print this help text and exit
                           (alias: -?)
@@ -192,6 +206,7 @@ The <input> 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 <file>]      write generated LLAIR to <file>
@@ -202,6 +217,8 @@ The <input> 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 <file>]            write report sexp to <file>, or to standard error
+                              if "-"
   [-trace <spec>]             enable debug tracing
   [-help]                     print this help text and exit
                               (alias: -?)
@@ -217,6 +234,7 @@ The <input> file must be binary LLAIR, such as produced by `sledge translate`.
 
 === flags ===
 
+  [-append-report]       append to report file
   [-bound <int>]         stop execution exploration at depth <int>
   [-colors]              enable printing in colors
   [-domain <string>]     select abstract domain; must be one of "sh" (default,
@@ -227,6 +245,8 @@ The <input> file must be binary LLAIR, such as produced by `sledge translate`.
   [-margin <cols>]       wrap debug tracing at <cols> columns
   [-no-simplify-states]  do not simplify states during symbolic execution
   [-preanalyze-globals]  pre-analyze global variables used by each function
+  [-report <file>]       write report sexp to <file>, or to standard error if
+                         "-"
   [-stats]               output performance statistics to stderr
   [-trace <spec>]        enable debug tracing
   [-help]                print this help text and exit
@@ -243,10 +263,13 @@ The <input> 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 <file>]  write generated textual LLAIR to <file>, or to
                               standard output if omitted
   [-margin <cols>]            wrap debug tracing at <cols> columns
+  [-report <file>]            write report sexp to <file>, or to standard error
+                              if "-"
   [-trace <spec>]             enable debug tracing
   [-help]                     print this help text and exit
                               (alias: -?)
@@ -262,8 +285,10 @@ The <input> file is interpreted as an SMT-LIB 2 benchmark.
 
 === flags ===
 
+  [-append-report]  append to report file
   [-colors]         enable printing in colors
   [-margin <cols>]  wrap debug tracing at <cols> columns
+  [-report <file>]  write report sexp to <file>, or to standard error if "-"
   [-trace <spec>]   enable debug tracing
   [-help]           print this help text and exit
                     (alias: -?)

sledge/sledge.opam

@@ -21,6 +21,7 @@ depends: [
   "fpath"
   "iter"
   "llvm" {= "8.0.0"}
+  "mtime"
   "ppx_compare"
   "ppx_hash"
   "shexp"

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

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)

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]