[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

@@ -9,10 +9,8 @@
 
 let unknown_call call =
   [%Trace.kprintf
-    (fun _ -> assert false)
+    Stop.on_unknown_call
-      "@\n\
+      "@\n@[<v 2>%a Unknown function call %a@;<1 2>@[%a@]@]@."
-       @[<v 2>%a Called unknown function %a executing instruction@;<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
+  let rep fs =
-    (loc access) pp access ;
+    Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Loc.pp
-  [%Trace.kprintf
+      (loc access) pp access
-    (fun _ -> assert false)
+  in
-      "@\n\
+  Format.printf "@\n@[<v 2>%t@]@." rep ;
-       @[<v 2>%a Invalid memory access@;<1 2>@[%a@]@;<1 2>@[{ %a@ }@]@]@."
+  [%Trace.printf
-      Loc.pp (loc access) pp access State_domain.pp state]
+    "@\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

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) ""]

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