From d58c81e83f5308c78bb403f9c88ab8b198ff4865 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 18 Sep 2022 15:54:22 -0400 Subject: [PATCH] wip: tracing system --- src/core/Sidekick_core.ml | 1 + src/core/dune | 3 +- src/core/t_tracer.ml | 9 ++++++ src/core/t_tracer.mli | 15 +++++++++ src/trace/dune | 6 ++++ src/trace/entry_id.ml | 7 +++++ src/trace/entry_id.mli | 9 ++++++ src/trace/entry_view.ml | 6 ++++ src/trace/sidekick_trace.ml | 29 +++++++++++++++++ src/trace/sink.ml | 62 +++++++++++++++++++++++++++++++++++++ src/trace/sink.mli | 20 ++++++++++++ src/trace/write_entry.ml | 8 +++++ src/trace/write_entry.mli | 27 ++++++++++++++++ src/trace/write_value.ml | 23 ++++++++++++++ src/trace/write_value.mli | 23 ++++++++++++++ 15 files changed, 247 insertions(+), 1 deletion(-) create mode 100644 src/core/t_tracer.ml create mode 100644 src/core/t_tracer.mli create mode 100644 src/trace/dune create mode 100644 src/trace/entry_id.ml create mode 100644 src/trace/entry_id.mli create mode 100644 src/trace/entry_view.ml create mode 100644 src/trace/sidekick_trace.ml create mode 100644 src/trace/sink.ml create mode 100644 src/trace/sink.mli create mode 100644 src/trace/write_entry.ml create mode 100644 src/trace/write_entry.mli create mode 100644 src/trace/write_value.ml create mode 100644 src/trace/write_value.mli diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 3ed9cdcc..32114358 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -22,6 +22,7 @@ module Term = struct include Sidekick_core_logic.Term include Sidekick_core_logic.T_builtins include T_printer + module Tracer = T_tracer end module Gensym = Gensym diff --git a/src/core/dune b/src/core/dune index 77bcd53e..b11693fe 100644 --- a/src/core/dune +++ b/src/core/dune @@ -2,4 +2,5 @@ (name Sidekick_core) (public_name sidekick.core) (flags :standard -open Sidekick_util) - (libraries containers iter sidekick.util sidekick.sigs sidekick.core-logic)) + (libraries containers iter sidekick.util sidekick.sigs sidekick.core-logic + sidekick.trace)) diff --git a/src/core/t_tracer.ml b/src/core/t_tracer.ml new file mode 100644 index 00000000..00fffdc1 --- /dev/null +++ b/src/core/t_tracer.ml @@ -0,0 +1,9 @@ +open Sidekick_core_logic +module Tr = Sidekick_trace +module T = Term + +type Tr.entry_view += private Def_term of { id: int } +type t = { sink: Tr.Sink.t; emitted: Tr.Entry_id.t T.Weak_map.t } + +let create ~sink () : t = { sink; emitted = T.Weak_map.create 16 } +let emit (self : t) (t : T.t) : Tr.Entry_id.t = assert false diff --git a/src/core/t_tracer.mli b/src/core/t_tracer.mli new file mode 100644 index 00000000..c6c150af --- /dev/null +++ b/src/core/t_tracer.mli @@ -0,0 +1,15 @@ +(** Emit terms in traces. + + Traces will contains terms, encoded as a DAG. Each subterm is its own + event, and gets a term identifier used in other subsequent entries + to refer to it. +*) + +open Sidekick_core_logic +module Tr = Sidekick_trace + +type Tr.entry_view += private Def_term of { id: int } +type t + +val create : sink:Tr.Sink.t -> unit -> t +val emit : t -> Term.t -> Tr.Entry_id.t diff --git a/src/trace/dune b/src/trace/dune new file mode 100644 index 00000000..aedce4a1 --- /dev/null +++ b/src/trace/dune @@ -0,0 +1,6 @@ +(library + (name Sidekick_trace) + (public_name sidekick.trace) + (synopsis "Trace system for sidekick.") + (flags :standard -open Sidekick_util) + (libraries containers iter sidekick.util sidekick.sigs sidekick.core-logic)) diff --git a/src/trace/entry_id.ml b/src/trace/entry_id.ml new file mode 100644 index 00000000..bbe7b8aa --- /dev/null +++ b/src/trace/entry_id.ml @@ -0,0 +1,7 @@ +type t = int + +let pp = Fmt.int + +module Internal_ = struct + let make x = x +end diff --git a/src/trace/entry_id.mli b/src/trace/entry_id.mli new file mode 100644 index 00000000..48ccf494 --- /dev/null +++ b/src/trace/entry_id.mli @@ -0,0 +1,9 @@ +type t = private int + +include Sidekick_sigs.PRINT with type t := t + +(**/*) +module Internal_ : sig + val make : int -> t +end +(**/*) diff --git a/src/trace/entry_view.ml b/src/trace/entry_view.ml new file mode 100644 index 00000000..060620cc --- /dev/null +++ b/src/trace/entry_view.ml @@ -0,0 +1,6 @@ + + +type t = .. +(** Extensible type, each entry uses its own. + + See {!Entry.t}. *) diff --git a/src/trace/sidekick_trace.ml b/src/trace/sidekick_trace.ml new file mode 100644 index 00000000..358bc2bd --- /dev/null +++ b/src/trace/sidekick_trace.ml @@ -0,0 +1,29 @@ +(** Tracing. + + Sidekick should be able to emit traces of some or all of the events + happening inside its components (SAT solver, SMT solver, theories, + etc.). + + Traces can be written to disk and read back later from another + process. + + The two initial intended use cases are: + + - proof production (trace all inferences; reconstruct a proof from them + starting from the inference of [false]) + - debugging (trace some inferences/internal states/partial models; + double check them later) + +*) + +open Sidekick_sigs + +(** {2 Exports} *) + +module Entry_view = Entry_view +module Write_value = Write_value +module Sink = Sink +module Entry_id = Entry_id + +type entry_id = Entry_id.t +type entry_view = Entry_view.t = .. diff --git a/src/trace/sink.ml b/src/trace/sink.ml new file mode 100644 index 00000000..8aefccdc --- /dev/null +++ b/src/trace/sink.ml @@ -0,0 +1,62 @@ +(** An IO sink for traces. + + A trace is emitted on the fly into a sink. The sink collects or + writes entries that are emitted into it. +*) + +module type S = sig + val emit : Write_value.t -> Entry_id.t +end + +type t = (module S) +(** Trace sink *) + +let[@inline] emit (module Sink : S) (v : Write_value.t) : Entry_id.t = + Sink.emit v + +let[@inline] emit' (self : t) v : unit = ignore (emit self v : Entry_id.t) + +let bencode_buf_ (buf:Buffer.t) (v:Write_value.t) : unit = + + let[@inline] char c = Buffer.add_char buf c in + let[@inline] str s = Buffer.add_string buf s in + let[@inline] int i = Printf.bprintf buf "%d" i in + + let rec enc_v (v:Write_value.t) : unit = + let module V = Write_value in + match v with + | V.Int i -> char 'i'; int i; char 'e' + | V.Bool true -> str "i1e" + | V.Bool false -> str "i0e" + | V.Str s | Bytes s -> + int (String.length s); + char ':'; + str s + | V.List l -> + char 'l'; + List.iter (fun v -> enc_v (v ())) l; + char 'e' + | V.Dict l -> + char 'd'; + List.iter (fun (k,v) -> + enc_v (V.string k); + enc_v (v ())) l; + char 'e' + in + enc_v v + +(** A sink that emits entries using Bencode into the given channel *) +let of_out_channel_using_bencode (oc: out_channel): t = + let id_ = ref 0 in + let buf = Buffer.create 128 in + (module struct + let emit (v:Write_value.t) = + assert (Buffer.length buf = 0); + let id = Entry_id.Internal_.make !id_ in + incr id_; + bencode_buf_ buf v; + Buffer.output_buffer oc buf; + Buffer.clear buf; + id + + end) diff --git a/src/trace/sink.mli b/src/trace/sink.mli new file mode 100644 index 00000000..6129758e --- /dev/null +++ b/src/trace/sink.mli @@ -0,0 +1,20 @@ +(** An IO sink for traces. + + A trace is emitted on the fly into a sink. The sink collects or + writes entries that are emitted into it. +*) + +module type S = sig + val emit : Write_value.t -> Entry_id.t +end + +type t = (module S) +(** Trace sink *) + +val emit : t -> Write_value.t -> Entry_id.t + +val emit' : t -> Write_value.t -> unit + +(** A sink that emits entries using Bencode into the given channel *) +val of_out_channel_using_bencode : out_channel -> t + diff --git a/src/trace/write_entry.ml b/src/trace/write_entry.ml new file mode 100644 index 00000000..52bec676 --- /dev/null +++ b/src/trace/write_entry.ml @@ -0,0 +1,8 @@ +type entry_view = Entry_view.t + +module type OPS = sig + val write : entry_view -> Write_value.t +end + +type ops = (module OPS) +type t = { view: entry_view; ops: ops } diff --git a/src/trace/write_entry.mli b/src/trace/write_entry.mli new file mode 100644 index 00000000..d9f966d8 --- /dev/null +++ b/src/trace/write_entry.mli @@ -0,0 +1,27 @@ +(** Entry to be written. + + This is used when producing a trace, to emit a new entry. +*) + +type entry_view = Entry_view.t + +(** Dynamic operations for {!t} *) +module type OPS = sig + val write : entry_view -> Write_value.t + + (* + val pp : entry_view Fmt.printer + *) + (* TODO: read *) +end + +type ops = (module OPS) + +type t = { view: entry_view; ops: ops } +(** A single entry to be written into the trace. + + A trace is consistuted of entries, numbered + from [0] to [n], in the order of their production. + The number has no semantics besides a form of + causal order. +*) diff --git a/src/trace/write_value.ml b/src/trace/write_value.ml new file mode 100644 index 00000000..be9f9bf6 --- /dev/null +++ b/src/trace/write_value.ml @@ -0,0 +1,23 @@ +(** Value writer. + + A [Writer.t] value, describes how to write some structured + data into a {!Sink.t}. It reflects the shape of the structured + data but does not commit to a particular serialization format. +*) + +type t = + | Bool of bool + | Str of string + | Bytes of string + | Int of int + | List of delayed list + | Dict of (string * delayed) list + +and delayed = unit -> t + +let bool b : t = Bool b +let int i : t = Int i +let string x : t = Str x +let bytes x : t = Bytes x +let list x : t = List x +let dict x : t = Dict x diff --git a/src/trace/write_value.mli b/src/trace/write_value.mli new file mode 100644 index 00000000..95ba14b3 --- /dev/null +++ b/src/trace/write_value.mli @@ -0,0 +1,23 @@ +(** Value writer. + + A [Writer.t] value, describes how to write some structured + data into a {!Sink.t}. It reflects the shape of the structured + data but does not commit to a particular serialization format. +*) + +type t = private + | Bool of bool + | Str of string + | Bytes of string + | Int of int + | List of delayed list + | Dict of (string * delayed) list + +and delayed = unit -> t + +val bool : bool -> t +val int : int -> t +val string : string -> t +val bytes : string -> t +val list : delayed list -> t +val dict : (string * delayed) list -> t