[litmus2desc] WIP: add litmus2desc

Author: fsestini

tools/litmus2desc/.ocamlformat

@@ -0,0 +1 @@
+disable = false

tools/litmus2desc/bin/dune

@@ -0,0 +1,6 @@
+(executable
+ (name main)
+ (public_name litmus2desc)
+ (flags
+  (:standard -w -42))
+ (libraries herdtools unix litmus2desc))

tools/litmus2desc/bin/main.ml

@@ -0,0 +1,46 @@
+module Top = Litmus2desc.Explainer
+
+let () =
+  let file_path = ref None in
+  let usage = "Usage: litmus2desc [options] FILE" in
+
+  let libdir = ref None in
+  let describe_regs = ref false in
+  let latex = ref false in
+  let options =
+    [
+      ( "-set-libdir",
+        Arg.String (fun s -> libdir := Some s),
+        "<path> set libdir" );
+      ( "--describe-regs",
+        Arg.Unit (fun () -> describe_regs := true),
+        "enable descriptions of register events. Default = disabled." );
+      ( "--latex",
+        Arg.Unit (fun () -> latex := true),
+        "Output test description as LaTeX. Default = disabled." );
+    ]
+  in
+  let process_arg arg =
+    match !file_path with
+    | None -> file_path := Some arg
+    | Some _ ->
+        prerr_endline "Only one FILE argument is allowed";
+        Arg.usage options usage;
+        exit 2
+  in
+
+  Arg.parse options process_arg usage;
+
+  let file_path =
+    match !file_path with
+    | Some p -> p
+    | None ->
+        prerr_endline "Missing FILE argument.";
+        Arg.usage options usage;
+        exit 2
+  in
+
+  let config =
+    Top.{ libdir = !libdir; describe_regs = !describe_regs; latex = !latex }
+  in
+  print_endline (Top.explain_test_path ~config file_path)

tools/litmus2desc/lib/EdgeGraph.ml

@@ -0,0 +1,51 @@
+type vertex = int
+type edge = { label : string; source : vertex; target : vertex }
+type t = { vertices : IntSet.t; succ : edge list IntMap.t }
+
+let make vertices edges =
+  let vertices =
+    List.fold_left (fun acc v -> IntSet.add v acc) IntSet.empty vertices
+  in
+  let vertices =
+    List.fold_left
+      (fun acc edge -> acc |> IntSet.add edge.source |> IntSet.add edge.target)
+      vertices edges
+  in
+  let succ =
+    List.fold_right
+      (fun edge acc ->
+        IntMap.update edge.source
+          (function
+            | None -> Some [ edge ] | Some edges -> Some (edge :: edges))
+          acc)
+      edges IntMap.empty
+  in
+  { vertices; succ }
+
+let outgoing_edges (g : t) (v : vertex) : edge list =
+  match IntMap.find_opt v g.succ with Some edges -> edges | None -> []
+
+let iter_simple_paths ~(src : vertex) ~(dst : vertex)
+    ~(pred : src:vertex -> tgt:vertex -> string -> bool)
+    ~(f : vertex list -> unit) (g : t) : unit =
+  if not (IntSet.mem src g.vertices && IntSet.mem dst g.vertices) then ()
+  else
+    let rec dfs visited path v =
+      if v = dst then f (List.rev (v :: path))
+      else
+        outgoing_edges g v
+        |> List.iter (fun edge ->
+            let next = edge.target in
+            if
+              (not (IntSet.mem next visited))
+              && pred ~src:edge.source ~tgt:next edge.label
+            then
+              let visited' = IntSet.add next visited in
+              dfs visited' (v :: path) next)
+    in
+    dfs (IntSet.singleton src) [] src
+
+let simple_paths_iter ~(src : int) ~(dst : int)
+    ~(pred : src:vertex -> tgt:vertex -> string -> bool) (g : t) :
+    int list Util.Iter.t =
+ fun f -> iter_simple_paths ~f ~src ~dst ~pred g

tools/litmus2desc/lib/EdgeGraph.mli

@@ -0,0 +1,12 @@
+type t
+type vertex = int
+type edge = { label : string; source : vertex; target : vertex }
+
+val make : vertex list -> edge list -> t
+
+val simple_paths_iter :
+  src:vertex ->
+  dst:vertex ->
+  pred:(src:vertex -> tgt:vertex -> string -> bool) ->
+  t ->
+  vertex list Util.Iter.t

tools/litmus2desc/lib/JsonGraph.ml

@@ -0,0 +1,179 @@
+(* JSON graph decoders for herd's JSON output. *)
+
+module Decoders = struct
+  module D = Decoders_yojson.Basic.Decode
+  open D.Infix
+  open Execution
+
+  let d_dir : dir D.decoder =
+    let* s = D.string in
+    match s with
+    | "R" -> D.succeed R
+    | "W" -> D.succeed W
+    | _ -> D.fail "invalid direction"
+
+  let d_event_ref : event_ref D.decoder =
+    let+ eiid = D.field "eiid" D.int in
+    { eiid }
+
+  let d_rel_edge : rel_edge D.decoder =
+    let* src = D.field "src" d_event_ref in
+    let+ tgt = D.field "tgt" d_event_ref in
+    { src; tgt }
+
+  let d_location : location D.decoder =
+    let* ty = D.field "type" D.string in
+    match ty with
+    | "reg" ->
+        let* proc = D.field "proc" D.int in
+        let+ reg_pretty = D.field "reg_pretty" D.string in
+        Reg { proc; reg_pretty }
+    | "global" ->
+        let+ global_pretty = D.field "global_pretty" D.string in
+        Global global_pretty
+    | _ -> D.fail "unknown location type"
+
+  let d_cst : cst D.decoder =
+    let* ty = D.field "type" D.string in
+    match ty with
+    | "concrete" ->
+        let+ scalar_pretty = D.field "scalar_pretty" D.string in
+        Concrete { scalar_pretty }
+    | "symbolic" ->
+        let+ symbol_pretty = D.field "symbol_pretty" D.string in
+        Symbolic { symbol_pretty }
+    | "pteval" ->
+        let* pteval_pretty = D.field "pteval_pretty" D.string in
+        let+ as_physical = D.maybe (D.field "as_physical" D.string) in
+        Pteval { pteval_pretty; as_physical }
+    | _ -> D.fail "unknown constant value type"
+
+  let d_value : value D.decoder =
+    let* ty = D.field "type" D.string in
+    match ty with
+    | "var" ->
+        let+ v = D.field "var" D.int in
+        Var v
+    | "val" ->
+        let d_val_pretty =
+          let+ vp = D.field "val_pretty" D.string in
+          Val_pretty vp
+        in
+        let d_val =
+          let+ v = D.field "val" d_cst in
+          Val v
+        in
+        D.one_of [ ("val_pretty", d_val_pretty); ("val", d_val) ]
+    | _ -> D.fail "unknown value type"
+
+  let d_mem_action : mem_action D.decoder =
+    let+ dir = D.field "dir" d_dir
+    and+ loc = D.field "loc" d_location
+    and+ value = D.field "value" d_value
+    and+ is_implicit = D.field_opt_or ~default:false "is_implicit" D.bool
+    and+ is_atomic = D.field_opt_or ~default:false "is_atomic" D.bool in
+    { dir; loc; value; is_implicit; is_atomic }
+
+  let d_reg_action : reg_action D.decoder =
+    let+ dir = D.field "dir" d_dir
+    and+ loc = D.field "loc" d_location
+    and+ value = D.field "value" d_value in
+    { dir; loc; value }
+
+  let d_action : action D.decoder =
+    let* ty = D.field "type" D.string in
+    match ty with
+    | "mem" ->
+        let+ c = d_mem_action in
+        Memory c
+    | "reg" ->
+        let+ c = d_reg_action in
+        Register c
+    | "barrier" ->
+        let+ barrier_pretty = D.field "barrier_pretty" D.string in
+        Barrier { barrier_pretty }
+    | "commit" ->
+        let+ commit = D.field "commit" D.string in
+        Commit { commit }
+    | "fault" -> D.succeed Fault
+    | _ -> D.fail "unknown action type"
+
+  let d_iiid : iiid D.decoder =
+    let d_id =
+      let* proc = D.field "proc" D.int in
+      let* poi = D.field "poi" D.int in
+      let+ inst_pretty = D.field "inst_pretty" D.string in
+      Index { proc; poi; inst_pretty }
+    in
+    let d_init_spurious =
+      let* s = D.string in
+      match s with
+      | "init" -> D.succeed Init
+      | "spurious" -> D.succeed Spurious
+      | _ -> D.fail "not a simple iiid string"
+    in
+    D.one_of [ ("init_spurious", d_init_spurious); ("id", d_id) ]
+
+  let d_event : event D.decoder =
+    let* act = D.field "act" d_action in
+    let* eiid = D.field "eiid" D.int in
+    let+ iiid = D.field "iiid" d_iiid in
+    { act; eiid; iiid }
+
+  open struct
+    open RFMap
+
+    let d_rfmap_src : src D.decoder =
+      let* ty = D.field "type" D.string in
+      match ty with
+      | "final" ->
+          let+ loc = D.field "loc" d_location in
+          Final loc
+      | "load" ->
+          let+ event = D.field "event" d_event_ref in
+          Load event
+      | _ -> D.fail "unknown rfmap src"
+
+    let d_rfmap_tgt : tgt D.decoder =
+      let* ty = D.field "type" D.string in
+      match ty with
+      | "init" -> D.succeed Init
+      | "store" ->
+          let+ event = D.field "event" d_event_ref in
+          Store event
+      | _ -> D.fail "unknown rfmap tgt"
+
+    let d_rfmap_edge : edge D.decoder =
+      let* src = D.field "src" d_rfmap_src in
+      let+ tgt = D.field "tgt" d_rfmap_tgt in
+      { src; tgt }
+  end
+
+  let d_viewed_before : viewed_before D.decoder =
+    D.key_value_pairs (D.list d_rel_edge)
+
+  let decode : t D.decoder =
+    let* events = D.field "events" (D.list d_event) in
+    let* iico_data = D.field "iico_data" (D.list d_rel_edge) in
+    let* iico_ctrl = D.field "iico_ctrl" (D.list d_rel_edge) in
+    let* speculated = D.field "speculated" (D.list d_event_ref) in
+    let* rfmap = D.field "rfmap" (D.list d_rfmap_edge) in
+    let* viewed_before = D.field "viewed_before" d_viewed_before in
+    let+ visible_po = D.maybe (D.field "visible_po" (D.list d_rel_edge)) in
+    {
+      events;
+      iico_data;
+      iico_ctrl;
+      speculated;
+      rfmap;
+      viewed_before;
+      visible_po;
+    }
+
+  let decode_list : t list D.decoder = D.list decode
+
+  let decode_string (s : string) : (t list, string) result =
+    D.decode_string decode_list s |> Result.map_error D.string_of_error
+end
+
+let decode_json_string = Decoders.decode_string

tools/litmus2desc/lib/JsonGraph.mli

@@ -0,0 +1 @@
+val decode_json_string : string -> (Execution.t list, string) result