[sledge] Refactor issue reporting to Report module

Summary:
Also for debugging support, note that analysis can be stopped after
reporting an attempt to call an unknown function with `sledge
-tReport.unknown_call` and likewise for invalid memory accesses with
`sledge -tReport.invalid_access`.

Reviewed By: mbouaziz

Differential Revision: D10389474

fbshipit-source-id: b006480d3

sledge/src/control.ml

@@ -166,20 +166,7 @@ let exec_throw stk state block exc =
 let exec_skip_func :
     stack -> Domain.t -> Llair.block -> Llair.jump -> Work.x =
  fun stk state block ({dst; args} as return) ->
-  Format.eprintf
-    "@\n\
-     @[<v 2>%a Called unknown function %a executing instruction@;<1 \
-     2>@[%a@]@]@."
-    Loc.pp
-    (Llair.Term.loc block.term)
-    (fun fs (term : Llair.Term.t) ->
-      match term with
-      | Call {call= {dst}} -> (
-        match Var.of_exp dst with
-        | Some var -> Var.pp_demangled fs var
-        | None -> Exp.pp fs dst )
-      | _ -> () )
-    block.term Llair.Term.pp block.term ;
+  Report.unknown_call block.term ;
   let return =
     if List.is_empty dst.params then return
     else
@@ -247,16 +234,7 @@ let exec_block : Llair.t -> stack -> Domain.t -> Llair.block -> Work.x =
   [%Trace.info "exec %a" Llair.Block.pp block] ;
   match Vector.fold_result ~f:Domain.exec_inst ~init:state block.cmnd with
   | Ok state -> exec_term pgm stk state block
-  | Error (q, i) ->
-      Format.printf
-        "@\n\
-         @[<v 2>%a Invalid memory access executing instruction@;<1 \
-         2>@[%a@]%t@]@."
-        Loc.pp (Llair.Inst.loc i) Llair.Inst.pp i (fun fs ->
-          if Version.debug then
-            Format.fprintf fs "@ from symbolic state@;<1 2>@[%a@]" Domain.pp
-              q ) ;
-      Work.skip
+  | Error (q, i) -> Report.invalid_access i q ; Work.skip
 
 let harness : Llair.t -> Work.t option =
  fun pgm ->

sledge/src/report.ml

@@ -0,0 +1,37 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Issue reporting *)
+
+let unknown_call call =
+  [%Trace.kprintf
+    (fun _ -> assert false)
+      "@\n\
+       @[<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) ->
+        match call with
+        | Call {call= {dst}} -> (
+          match Var.of_exp dst with
+          | Some var -> Var.pp_demangled fs var
+          | None -> Exp.pp fs dst )
+        | _ -> () )
+      call Llair.Term.pp call]
+
+let invalid_access inst state =
+  Format.printf
+    "@\n\
+     @[<v 2>%a Invalid memory access executing instruction@;<1 2>@[%a@]@]@."
+    Loc.pp (Llair.Inst.loc inst) Llair.Inst.pp inst ;
+  [%Trace.kprintf
+    (fun _ -> assert false)
+      "@\n\
+       @[<v 2>%a Invalid memory access executing instruction@;<1 2>@[%a@]@ \
+       from symbolic state@;<1 2>@[{ %a@ }@]@]@."
+      Loc.pp (Llair.Inst.loc inst) Llair.Inst.pp inst Domain.pp state]

sledge/src/report.mli

@@ -0,0 +1,11 @@
+(*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Issue reporting *)
+
+val unknown_call : Llair.term -> unit
+val invalid_access : Llair.inst -> Domain.t -> unit