[pudge] spit out sledge replay tests

Summary: Also add an infer option to enable sledge timers.

Reviewed By: jberdine

Differential Revision: D20871159

fbshipit-source-id: d4ea0e9f2

infer/man/man1/infer-full.txt

@@ -1694,6 +1694,11 @@ INTERNAL OPTIONS
        --skip-translation-headers-reset
            Set --skip-translation-headers to the empty list.
 
+       --sledge-timers
+           Activates: Enable debug timing info from sledge on stderr (you
+           probably want --no-progress-bar as well). (Conversely:
+           --no-sledge-timers)
+
        --source-files-filter-reset
            Cancel the effect of --source-files-filter.
 

infer/src/base/Config.ml

@@ -2008,6 +2008,12 @@ and skip_translation_headers =
     ~meta:"path_prefix" "Ignore headers whose path matches the given prefix"
 
 
+and sledge_timers =
+  CLOpt.mk_bool ~long:"sledge-timers"
+    "Enable debug timing info from sledge on stderr (you probably want $(b,--no-progress-bar) as \
+     well)."
+
+
 and source_preview =
   CLOpt.mk_bool ~long:"source-preview" ~default:true
     ~in_help:InferCommand.[(Explore, manual_explore_bugs)]
@@ -2935,6 +2941,8 @@ and skip_duplicated_types = !skip_duplicated_types
 
 and skip_translation_headers = !skip_translation_headers
 
+and sledge_timers = !sledge_timers
+
 and source_preview = !source_preview
 
 and source_files = !source_files

infer/src/base/Config.mli

@@ -525,6 +525,8 @@ val skip_duplicated_types : bool
 
 val skip_translation_headers : string list
 
+val sledge_timers : bool
+
 val source_files : bool
 
 val source_files_cfg : bool

infer/src/pulse/Pulse.ml

@@ -211,6 +211,23 @@ module DisjunctiveTransferFunctions =
 
 module DisjunctiveAnalyzer = AbstractInterpreter.MakeWTO (DisjunctiveTransferFunctions)
 
+(* Output cases that sledge was unhappy with in files for later replay or inclusion as sledge test
+   cases. We create one file for each PID to avoid all analysis processes racing on writing to the same
+   file. *)
+let sledge_test_fmt =
+  lazy
+    (let sledge_test_output =
+       Out_channel.create
+         ( ResultsDir.get_path Debug
+         ^/ Printf.sprintf "sledge_test-%d.ml" (Pid.to_int (Unix.getpid ())) )
+     in
+     let f = F.formatter_of_out_channel sledge_test_output in
+     Epilogues.register ~description:"closing sledge debug fd" ~f:(fun () ->
+         F.pp_print_flush f () ;
+         Out_channel.close sledge_test_output ) ;
+     f )
+
+
 let checker {Callbacks.exe_env; summary} =
   let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in
   AbstractValue.init () ;
@@ -229,3 +246,28 @@ let checker {Callbacks.exe_env; summary} =
         summary
   | None ->
       summary
+  | exception exn ->
+      (* output sledge replay tests, see comment on [sledge_test_fmt] *)
+      IExn.reraise_if exn ~f:(fun () ->
+          match Exn.sexp_of_t exn with
+          | List [exn; replay] ->
+              let exn = Error.t_of_sexp exn in
+              L.internal_error "Analysis of %a FAILED:@\n@[%a@]@\n" Procname.pp
+                (Procdesc.get_proc_name pdesc) Error.pp exn ;
+              F.fprintf (Lazy.force sledge_test_fmt)
+                "@\n\
+                \    let%%expect_test _ =@\n\
+                \      Equality.replay@\n\
+                \        {|%a|} ;@\n\
+                \      [%%expect {| |}]@\n\
+                 @\n\
+                 %!"
+                Sexp.pp_hum replay ;
+              false
+          | _ | (exception _) ->
+              (* re-raise original exception *)
+              true ) ;
+      summary
+
+
+let () = Sledge.Timer.enabled := Config.sledge_timers