From 8ac22675955d3f33c55e1c9420666f1a8fa9f43a Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 21 Oct 2021 20:33:10 -0400
Subject: [PATCH] add a simple binary to dump proof traces

---
 proof-trace-dump.sh                      |  2 ++
 src/main/main.ml                         | 16 +++++++----
 src/proof-trace-dump/dune                |  6 ++++
 src/proof-trace-dump/proof_trace_dump.ml | 35 ++++++++++++++++++++++++
 4 files changed, 53 insertions(+), 6 deletions(-)
 create mode 100755 proof-trace-dump.sh
 create mode 100644 src/proof-trace-dump/dune
 create mode 100644 src/proof-trace-dump/proof_trace_dump.ml

diff --git a/proof-trace-dump.sh b/proof-trace-dump.sh
new file mode 100755
index 00000000..b4b96e4c
--- /dev/null
+++ b/proof-trace-dump.sh
@@ -0,0 +1,2 @@
+#!/usr/bin/env sh
+exec dune exec --profile=release src/proof-trace-dump/proof_trace_dump.exe -- $@
diff --git a/src/main/main.ml b/src/main/main.ml
index 210c68dc..14d630e5 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -31,6 +31,7 @@ let p_gc_stat = ref false
 let p_progress = ref false
 let proof_file = ref ""
 let proof_store_memory = ref false
+let proof_store_file = ref ""
 
 (* Arguments parsing *)
 let int_arg r arg =
@@ -71,6 +72,7 @@ let argspec = Arg.align [
     "--proof", Arg.Set p_proof, " print proof";
     "--no-proof", Arg.Clear p_proof, " do not print proof";
     "--proof-in-memory", Arg.Set proof_store_memory, " store temporary proof in memory";
+    "--proof-trace-file", Arg.Set_string proof_store_file, " store temporary proof in given file (no cleanup)";
     "-o", Arg.Set_string proof_file, " file into which to output a proof";
     "--model", Arg.Set p_model, " print model";
     "--no-model", Arg.Clear p_model, " do not print model";
@@ -104,13 +106,15 @@ let main_smt () : _ result =
 
   (* call [k] with the name of a temporary proof file, and cleanup if necessary *)
   let run_with_tmp_file k =
+    (* TODO: use memory writer if [!proof_store_memory] *)
     if enable_proof_ then (
-      let file = ".sidekick-trace.dat" in
-      k file
-      (*  TODO
-      CCIO.File.with_temp
-        ~temp_dir:"." ~prefix:".sidekick-proof" ~suffix:".dat" k
-          *)
+      if !proof_store_file <> "" then (
+        let file = !proof_store_file in
+        k file
+      ) else (
+        CCIO.File.with_temp
+          ~temp_dir:"." ~prefix:".sidekick-proof" ~suffix:".dat" k
+      )
     ) else (
       k "/dev/null"
     )
diff --git a/src/proof-trace-dump/dune b/src/proof-trace-dump/dune
new file mode 100644
index 00000000..d4b8e4ec
--- /dev/null
+++ b/src/proof-trace-dump/dune
@@ -0,0 +1,6 @@
+
+(executable
+  (name proof_trace_dump)
+  (modes native)
+  (libraries containers sidekick.util sidekick-base.proof-trace)
+  (flags :standard -w -32 -warn-error -a+8 -open Sidekick_util))
diff --git a/src/proof-trace-dump/proof_trace_dump.ml b/src/proof-trace-dump/proof_trace_dump.ml
new file mode 100644
index 00000000..0a1353c5
--- /dev/null
+++ b/src/proof-trace-dump/proof_trace_dump.ml
@@ -0,0 +1,35 @@
+
+module CS = Chunk_stack
+module Proof_ser = Sidekick_base_proof_trace.Proof_ser
+
+let parse_file (file:string) : unit =
+  Log.debugf 2 (fun k->k"parsing file %S" file);
+
+  CS.Reader.with_file_backward file @@ fun reader ->
+
+  let n = ref 0 in
+  let rec display_steps () =
+    CS.Reader.next reader
+      ~finish:(fun () -> ())
+      ~yield:(fun b i _len ->
+          let decode = {Proof_ser.Bare.Decode.bs=b; off=i} in
+          let step = Proof_ser.Step.decode decode in
+          incr n;
+          Format.printf "@[<2>%a@]@." Proof_ser.Step.pp step;
+          display_steps();
+        );
+  in
+  display_steps();
+  Format.printf "read %d steps@." !n;
+  ()
+
+let () =
+  let file = ref "" in
+  let opts = [
+    "--bt", Arg.Unit (fun () -> Printexc.record_backtrace true), " enable stack traces";
+    "-d", Arg.Int Log.set_debug, "<lvl> sets the debug verbose level";
+  ] |> Arg.align in
+  Arg.parse opts (fun f -> file := f) "proof-trace-dump <file>";
+  if !file = "" then failwith "please provide a file";
+
+  parse_file !file