From 1908077aa9c50e95b24d18115bfa40c53fe78254 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 1 Jul 2019 07:16:47 -0700
Subject: [PATCH] [sledge] Include alarms in debug trace

Summary:
Currently alarms are reported to stdout while the debug trace is
written to stderr. This makes synchronizing the two difficult. With
this diff, the alarm reports can also be included in the debug trace,
and analysis can be stopped when an alarm is encountered by tracing
the `Stop` module, e.g.:
```
sledge -trace Report+Stop.on_invalid_access
```

Reviewed By: kren1

Differential Revision: D16072611

fbshipit-source-id: 32c3639a2
---
 sledge/src/report.ml | 21 ++++++++++-----------
 sledge/src/stop.ml   | 11 +++++++++++
 sledge/src/stop.mli  | 11 +++++++++++
 3 files changed, 32 insertions(+), 11 deletions(-)
 create mode 100644 sledge/src/stop.ml
 create mode 100644 sledge/src/stop.mli

diff --git a/sledge/src/report.ml b/sledge/src/report.ml
index f5e135cd0..3a5ae8d28 100644
--- a/sledge/src/report.ml
+++ b/sledge/src/report.ml
@@ -9,10 +9,8 @@
 
 let unknown_call call =
   [%Trace.kprintf
-    (fun _ -> assert false)
-      "@\n\
-       @[<v 2>%a Called unknown function %a executing instruction@;<1 \
-       2>@[%a@]@]@."
+    Stop.on_unknown_call
+      "@\n@[<v 2>%a Unknown function call %a@;<1 2>@[%a@]@]@."
       (fun fs call -> Loc.pp fs (Llair.Term.loc call))
       call
       (fun fs (call : Llair.Term.t) ->
@@ -25,13 +23,14 @@ let unknown_call call =
       call Llair.Term.pp call]
 
 let invalid_access state pp access loc =
-  Format.printf "@\n@[<v 2>%a Invalid memory access@;<1 2>@[%a@]@]@." Loc.pp
-    (loc access) pp access ;
-  [%Trace.kprintf
-    (fun _ -> assert false)
-      "@\n\
-       @[<v 2>%a Invalid memory access@;<1 2>@[%a@]@;<1 2>@[{ %a@ }@]@]@."
-      Loc.pp (loc access) pp access State_domain.pp state]
+  let rep fs =
+    Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Loc.pp
+      (loc access) pp access
+  in
+  Format.printf "@\n@[<v 2>%t@]@." rep ;
+  [%Trace.printf
+    "@\n@[<v 2>%t@;<1 2>@[{ %a@ }@]@]@." rep State_domain.pp state] ;
+  Stop.on_invalid_access ()
 
 let invalid_access_inst state inst =
   invalid_access state Llair.Inst.pp inst Llair.Inst.loc
diff --git a/sledge/src/stop.ml b/sledge/src/stop.ml
new file mode 100644
index 000000000..db4f3377c
--- /dev/null
+++ b/sledge/src/stop.ml
@@ -0,0 +1,11 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Stop analysis when encountering issues *)
+
+let on_unknown_call _ = [%Trace.kprintf (fun _ -> assert false) ""]
+let on_invalid_access _ = [%Trace.kprintf (fun _ -> assert false) ""]
diff --git a/sledge/src/stop.mli b/sledge/src/stop.mli
new file mode 100644
index 000000000..6f9b4e6c6
--- /dev/null
+++ b/sledge/src/stop.mli
@@ -0,0 +1,11 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Stop analysis when encountering issues *)
+
+val on_unknown_call : 'a -> unit
+val on_invalid_access : 'a -> unit