diff --git a/tools/dune b/tools/dune index 58519f8dc8..e00fa46ac8 100644 --- a/tools/dune +++ b/tools/dune @@ -10,7 +10,8 @@ mheader splitdot trTrue - lexMiaou) + lexMiaou + lexLogSelect) (executables (names @@ -54,7 +55,8 @@ miaou cat2lisp dot2desc - cat2table) + cat2table + mlogselect) (public_names mfind7 moutcomes7 @@ -96,7 +98,8 @@ miaou7 cat2lisp dot2desc7 - cat2table7) + cat2table7 + mlogselect7) (libraries herdtools unix str) (modules_without_implementation arch_tools)) diff --git a/tools/lexLogSelect.mli b/tools/lexLogSelect.mli new file mode 100644 index 0000000000..90ab15a166 --- /dev/null +++ b/tools/lexLogSelect.mli @@ -0,0 +1,19 @@ +(****************************************************************************) +(* the diy toolsuite *) +(* *) +(* Jade Alglave, University College London, UK. *) +(* Luc Maranget, INRIA Paris-Rocquencourt, France. *) +(* *) +(* Copyright 2026-present Institut National de Recherche en Informatique et *) +(* en Automatique and the authors. All rights reserved. *) +(* *) +(* This software is governed by the CeCILL-B license under French law and *) +(* abiding by the rules of distribution of free software. You can use, *) +(* modify and/ or redistribute the software under the terms of the CeCILL-B *) +(* license as circulated by CEA, CNRS and INRIA at the following URL *) +(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *) +(****************************************************************************) + +(** Fast lexing of logs, for selection *) + +val from_chan : (string -> bool) -> in_channel -> unit diff --git a/tools/lexLogSelect.mll b/tools/lexLogSelect.mll new file mode 100644 index 0000000000..a4658971fb --- /dev/null +++ b/tools/lexLogSelect.mll @@ -0,0 +1,91 @@ +(****************************************************************************) +(* the diy toolsuite *) +(* *) +(* Jade Alglave, University College London, UK. *) +(* Luc Maranget, INRIA Paris-Rocquencourt, France. *) +(* *) +(* Copyright 2026-present Institut National de Recherche en Informatique et *) +(* en Automatique and the authors. All rights reserved. *) +(* *) +(* This software is governed by the CeCILL-B license under French law and *) +(* abiding by the rules of distribution of free software. You can use, *) +(* modify and/ or redistribute the software under the terms of the CeCILL-B *) +(* license as circulated by CEA, CNRS and INRIA at the following URL *) +(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *) +(****************************************************************************) + +(** Extract records from herd/litmus/msum logs *) + +(* + * The extraction is a bit complicated by the variety of log formats... + * + Fortunately all records starts with `Test `, where + * is the name of the test. + * + Unfortunately, the format of record end differ: + * - The records produced by herd and msum end at the first empty line. + * - The records produced by litmus include an empty line that' + * follows the validation tag (Ok/No). The end at the "Time" + * information that always follow the Hash metadata. + * The output of mlogselect adopts the convention of herd and msum. + *) +{ +open LexMisc + +let outline = print_endline + +type st = { inside:bool; hash_seen:bool; } +let st_false = { inside=false; hash_seen=false; } +let st_true = { inside=true; hash_seen=false; } +} + +let digit = [ '0'-'9' ] +let alpha = [ 'a'-'z' 'A'-'Z'] +let name = (alpha|'_'|'.'|'$') (alpha|digit|'_'| '.')* +let blank = [' ' '\t'] +let testname = (alpha|digit|'_' | '/' | '.' | '-' | '+' | '[' | ']' | ':')+ +let nl = '\r'?'\n' +let validation = "Ok"|"No" + +rule main ok st = parse +| "Test" blank+ (testname as t) + (blank+ name)? as line nl + { incr_lineno lexbuf ; + let st = if ok t then st_true else st_false in + if st.inside then outline line ; + main ok st lexbuf } +| nl (* An empty line ends one test log in herd/msum logs *) + { incr_lineno lexbuf ; + if st.inside then outline "" ; + main ok st_false lexbuf } +| validation as line nl nl +(* Unless the empty line follows a validation tag, + as in some litmus logs *) + { incr_lineno lexbuf ; incr_lineno lexbuf ; + if st.inside then outline line ; + main ok st lexbuf } +| ['h''H']['a''A']['s''S']['h''H'] + blank* '=' blank* [^' ''\t''\n''\r']+ blank* as line nl +(* Detect hash metadata *) + { incr_lineno lexbuf ; + if st.inside then outline line ; + main ok {st with hash_seen=true; } lexbuf } +| "Time" blank+ testname blank+ (digit|'.')+ blank* as line nl +(* Detect timing information that ends records in litmus logs *) + { incr_lineno lexbuf ; + if st.inside then outline line ; + if st.hash_seen then begin (* End of record, if follows hash metadata *) + if st.inside then outline "" ; (* Add empty line *) + main ok st_false lexbuf + end else + main ok st lexbuf } +| [^'\n''\r']+ as line nl + { incr_lineno lexbuf ; + if st.inside then outline line ; + main ok st lexbuf } +| [^'\n''\r']* as line eof + { if st.inside && line <> "" then outline line } + +{ + +let from_chan ok chan = main ok st_false @@ Lexing.from_channel chan + +} diff --git a/tools/mlogselect.ml b/tools/mlogselect.ml new file mode 100644 index 0000000000..fba10e8e29 --- /dev/null +++ b/tools/mlogselect.ml @@ -0,0 +1,65 @@ +(****************************************************************************) +(* the diy toolsuite *) +(* *) +(* Jade Alglave, University College London, UK. *) +(* Luc Maranget, INRIA Paris-Rocquencourt, France. *) +(* *) +(* Copyright 2026-present Institut National de Recherche en Informatique et *) +(* en Automatique and the authors. All rights reserved. *) +(* *) +(* This software is governed by the CeCILL-B license under French law and *) +(* abiding by the rules of distribution of free software. You can use, *) +(* modify and/ or redistribute the software under the terms of the CeCILL-B *) +(* license as circulated by CEA, CNRS and INRIA at the following URL *) +(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *) +(****************************************************************************) + +(* Extract some records from logs. *) +open Printf +open OptNames + +let prog = + if Array.length Sys.argv > 0 then Sys.argv.(0) + else "mlogelect" + +let arg = ref None + +let () = + Arg.parse + OptNames.parse_withselect + (fun s -> + arg := + match !arg with + | None -> Some s + | Some _ -> raise (Arg.Bad "one argument at most")) + (sprintf "usage: %s [options]* log?" prog) + +(* Read names *) + +module Check = + CheckName.Make + (struct + let verbose = 0 + let rename = [] + let select = !select + let names = !names + let oknames = !oknames + let excl = !excl + let nonames = !nonames + end) + +let zyva () = + match !arg with + | None -> + LexLogSelect.from_chan Check.ok stdin + | Some f -> + Misc.input_protect + (LexLogSelect.from_chan Check.ok) + f + +let () = + try zyva () + with + | Misc.(Fatal msg|UserError msg) -> + Warn.warn_always "Fatal error: %s" msg + | _ -> assert false diff --git a/tools/tests/mlogselect/dune b/tools/tests/mlogselect/dune new file mode 100644 index 0000000000..d545778512 --- /dev/null +++ b/tools/tests/mlogselect/dune @@ -0,0 +1,9 @@ +(cram + (deps + %{bin:mlogselect7} + %{bin:msum7} + %{bin:herd7} + (glob_files %{workspace_root}/herd/tests/instructions/X86_64/*.litmus) + (glob_files %{workspace_root}/doc/SB-PPC.litmus) + (glob_files %{workspace_root}/doc/SB-PPC*.log) + (source_tree %{workspace_root}/herd/libdir))) diff --git a/tools/tests/mlogselect/mlogselect.t b/tools/tests/mlogselect/mlogselect.t new file mode 100644 index 0000000000..20543f41ea --- /dev/null +++ b/tools/tests/mlogselect/mlogselect.t @@ -0,0 +1,87 @@ +Extract test output from litmus log + $ mlogselect7 -oknames SB-PPC ../../../doc/SB-PPC.log + Test SB-PPC Allowed + Histogram (3 states) + 1784 *>0:r3=0; 1:r3=0; + 498564:>0:r3=1; 1:r3=0; + 499652:>0:r3=0; 1:r3=1; + Ok + Witnesses + Positive: 1784, Negative: 998216 + Condition exists (0:r3=0 /\ 1:r3=0) is validated + Hash=4edecf6abc507611612efaecc1c4a9bc + Observation SB-PPC Sometimes 1784 998216 + Time SB-PPC 0.55 + +Extract test output from msum log + $ msum7 ../../../doc/SB-PPC*.log 2>/dev/null | mlogselect7 -select ../../../doc/SB-PPC.litmus + Test SB-PPC Allow + Histogram (3 states) + 3549 :> 0:r3=0; 1:r3=0; + 999146 :> 0:r3=0; 1:r3=1; + 997305 :> 0:r3=1; 1:r3=0; + Ok + Witnesses + Positive: 3549 Negative: 1996451 + Condition exists (0:r3=0 /\ 1:r3=0) is validated + Hash=4edecf6abc507611612efaecc1c4a9bc + Time SB-PPC 1.12 + +Extract test output from herd log + $ for i in $(seq 1 2 9); do echo "A00$i"; done > NAMES + $ herd7 -set-libdir ../../../herd/libdir ../../../herd/tests/instructions/X86_64/*.litmus | mlogselect7 -names NAMES -nonames A003,A004 -oknames A012 + Test A001 Required + States 1 + 0:rip=0; + Ok + Witnesses + Positive: 1 Negative: 0 + Condition forall (0:rip=0) + Observation A001 Always 1 0 + Time A001 0.00 + Hash=5586d6c213112d3683c915b4d7bb700a + + Test A005 Required + States 1 + 0:rax=0; + Ok + Witnesses + Positive: 1 Negative: 0 + Condition forall (0:rax=0) + Observation A005 Always 1 0 + Time A005 0.00 + Hash=33e970980643a03ccf92e4989259cd01 + + Test A007 Required + States 1 + 0:rax=4; + Ok + Witnesses + Positive: 1 Negative: 0 + Condition forall (0:rax=4) + Observation A007 Always 1 0 + Time A007 0.00 + Hash=a335aafc9060d9b8c4320424ba909740 + + Test A009 Required + States 1 + 0:rcx=-1; + Ok + Witnesses + Positive: 1 Negative: 0 + Condition forall (0:rcx=-1) + Observation A009 Always 1 0 + Time A009 0.00 + Hash=7ca3c35015d75a877ccf509d75062e79 + + Test A012 Required + States 1 + [x]=1; + Ok + Witnesses + Positive: 1 Negative: 0 + Condition forall ([x]=1) + Observation A012 Always 1 0 + Time A012 0.00 + Hash=3b021e40517dcff1f1cb8894d645b677 +