Z3 Tracing

src/choice_monad.ml

@@ -22,7 +22,9 @@ let check (sym_bool : vbool) (state : Thread.t) : bool =
     Format.printf "CHECK:@.";
     List.iter (fun c -> print_endline (Encoding.Expression.to_string c)) check;
     let module Solver = (val solver_module) in
-    let r = Solver.check solver check in
+    let r =
+      Tracing.with_ev Tracing.check (fun () -> Solver.check solver check)
+    in
     let msg = if r then "KO" else "OK" in
     Format.printf "/CHECK %s@." msg;
     not r
@@ -40,8 +42,14 @@ let eval_choice (sym_bool : vbool) (state : Thread.t) : (bool * Thread.t) list =
   | _ -> (
     let no = Symbolic_value.S.Bool.not sym_bool in
     let module Solver = (val solver_module) in
-    let sat_true = Solver.check s (sym_bool :: pc) in
-    let sat_false = Solver.check s (no :: pc) in
+    let sat_true =
+      Tracing.with_ev Tracing.check_true (fun () ->
+          Solver.check s (sym_bool :: pc))
+    in
+    let sat_false =
+      Tracing.with_ev Tracing.check_false (fun () ->
+          Solver.check s (no :: pc))
+    in
     match (sat_true, sat_false) with
     | false, false -> []
     | true, false -> [ (true, state) ]
@@ -115,9 +123,16 @@ let eval_choice_i32 (sym_int : vint32) (state : Thread.t) :
     let module Solver = (val solver_module) in
     let rec find_values values =
       let additionnal = List.map (not_value sym) values in
-      if not (Solver.check solver (additionnal @ pc)) then []
+      if
+        not
+          (Tracing.with_ev Tracing.check (fun () ->
+               Solver.check solver (additionnal @ pc) ) )
+      then []
       else begin
-        let model = Solver.model ~symbols:[ sym ] solver in
+        let model =
+          Tracing.with_ev Tracing.model (fun () ->
+              Solver.model ~symbols:[ sym ] solver )
+        in
         match model with
         | None -> assert false (* ? *)
         | Some model -> (

src/dune

@@ -54,14 +54,15 @@
   syntax
   text
   thread
+  tracing
   trap
   typecheck
   types
   value_intf
   v
   wutf8)
- (private_modules convert lexer menhir_parser spectest wutf8)
- (libraries encoding integers menhirLib ocaml_intrinsics ppxlib sedlex uutf)
+ (private_modules convert lexer menhir_parser spectest wutf8 tracing)
+ (libraries encoding integers menhirLib ocaml_intrinsics ppxlib sedlex uutf runtime_events)
  (preprocess
   (pps sedlex.ppx))
  (instrumentation

src/tracing.ml

@@ -0,0 +1,28 @@
+type Runtime_events.User.tag += Solver_check
+
+type Runtime_events.User.tag += Solver_check_true
+
+type Runtime_events.User.tag += Solver_check_false
+
+type Runtime_events.User.tag += Solver_model
+
+let check =
+  Runtime_events.User.register "solver_check" Solver_check
+    Runtime_events.Type.span
+
+let check_true =
+  Runtime_events.User.register "solver_check_true" Solver_check_true
+    Runtime_events.Type.span
+
+let check_false =
+  Runtime_events.User.register "solver_check_false" Solver_check_false
+    Runtime_events.Type.span
+
+let model =
+  Runtime_events.User.register "solver_model" Solver_model
+    Runtime_events.Type.span
+
+let with_ev ev f =
+  Runtime_events.User.write ev Runtime_events.Type.Begin;
+  Fun.protect f ~finally:(fun () ->
+      Runtime_events.User.write ev Runtime_events.Type.End )