From 7817a87e32fecf683610f41c68b5cd3b3c74d25d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 21 Apr 2021 15:34:07 -0700 Subject: [PATCH] [sledge] Support stopping on first report in release mode Summary: Specifying that sledge should stop execution when the first report is made via e.g. `sledge l a -t Stop` currently only works when debug tracing is enabled. This diff fixes this so that `-t Stop` also works for the release build. Reviewed By: jvillard Differential Revision: D27828753 fbshipit-source-id: dd7511ff1 --- sledge/cli/sledge_cli.ml | 3 ++- sledge/src/stop.ml | 6 ++++-- sledge/src/stop.mli | 2 ++ 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml index 2e46cc9e9..e5d2d8b9f 100644 --- a/sledge/cli/sledge_cli.ml +++ b/sledge/cli/sledge_cli.ml @@ -56,6 +56,7 @@ let command ~summary ?readme param = | Assert_failure _ as exn -> Report.InternalError (Sexp.to_string_hum (sexp_of_exn exn)) | Failure msg -> Report.InternalError msg + | Stop.Stop -> Report.safe_or_unsafe () | exn -> Report.UnknownError (Printexc.to_string exn) in Report.status (status_of_exn exn) ; @@ -143,8 +144,8 @@ let analyze = let module Analysis = Control.Make (Opts) (Dom) in Domain_sh.simplify_states := not no_simplify_states ; Option.iter dump_query ~f:(fun n -> Solver.dump_query := n) ; + at_exit (fun () -> Report.coverage pgm) ; Analysis.exec_pgm pgm ; - Report.coverage pgm ; Report.safe_or_unsafe () let analyze_cmd = diff --git a/sledge/src/stop.ml b/sledge/src/stop.ml index 29794ad94..dcad8c0cd 100644 --- a/sledge/src/stop.ml +++ b/sledge/src/stop.ml @@ -7,5 +7,7 @@ (** Stop analysis when encountering issues *) -let on_unknown_call _ = [%Trace.kprintf (fun _ -> assert false) ""] -let on_alarm _ = [%Trace.kprintf (fun _ -> assert false) ""] +exception Stop + +let on_unknown_call _ = Trace.kprintf __FUNCTION__ (fun _ -> raise Stop) "" +let on_alarm _ = Trace.kprintf __FUNCTION__ (fun _ -> raise Stop) "" diff --git a/sledge/src/stop.mli b/sledge/src/stop.mli index d78875ed6..1846cd8c1 100644 --- a/sledge/src/stop.mli +++ b/sledge/src/stop.mli @@ -7,5 +7,7 @@ (** Stop analysis when encountering issues *) +exception Stop + val on_unknown_call : 'a -> unit val on_alarm : 'a -> unit