Skip to content

[tools/mprog7] Add ability to read input litmus test from stdin - #1980

Open
fsestini wants to merge 4 commits into
herd:masterfrom
fsestini:mprog-stdin
Open

[tools/mprog7] Add ability to read input litmus test from stdin#1980
fsestini wants to merge 4 commits into
herd:masterfrom
fsestini:mprog-stdin

Conversation

@fsestini

@fsestini fsestini commented Sep 2, 2026

Copy link
Copy Markdown
Collaborator

This PR adds the conventional - operand to mprog7 for reading one litmus test from standard input. For example:

$ cat ./tools/tests/mprog/stdin.t/A.litmus
AArch64 A
{}
P0;
MOV X0,#1;
exists (0:X0=1)
$ cat ./tools/tests/mprog/stdin.t/A.litmus | mprog7 -mode text -
AArch64 A
{
}
 P0        ;
 MOV X0,#1 ;

exists (0:X0=1)

This functionality can be quite handy when using mprog7 as a litmus test formatter, for example within an editor like vim.

  • As before this PR, absent - or positional arguments, stdin is interpreted as a list of filenames.
  • - may be used alongside file paths.
  • - can only be specified at most once.
  • A - read from a filename list (be it from stdin or from a @list file) is interpreted as a literal filename.
  • When -o DIR is specified, the litmus test read from stdin input is saved as DIR/stdin.litmus.

This PR updates the input mechanism of mprog7 to support the new stdin operand and brings its batch error handling in line with conventional CLI behaviour. Previously, errors associated with an individual input were reported but not reflected in the exit code, so a batch could finish with status zero even when one or more inputs had failed. With this PR, mprog7 now retains its useful behaviour of continuing batch processing of multiple inputs, while recording whether any input failed and returning status 1 after the batch if so. Command-line errors and failures encountered while opening an @list continue to return status 2.

Comment thread tools/mprog.ml
Misc.iter_argv_or_stdin
(fun fname ->
try X.zyva fname with
| Misc.Exit -> ()

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've removed this line as I did not understand why it was there: no code path downstream of mprog7 seems to be raising Misc.Exit, and even if it does, I'm not sure it's a good idea to silently swallow the exception anyway.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well, I do not know if the handler is appropriate, probably not. The usual reaction to Misc.Exit is not doing anything, assuming that the error has been flagged before, or that there is no error to flag, See tools/mnames.ml for an example of the second possibility.

Comment thread tools/mprog.ml
Comment on lines -335 to -337
| e ->
Printf.eprintf "\nFatal: %a Adios\n" Pos.pp_pos0 fname ;
raise e)

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've removed this as generally I'm not a fan of catch-all branches, and this branch doesn't seem to really add much to the error it catches, in terms of error message. In fact, catching and rethrowing exceptions risks garbling the stack trace of the original exception, which makes debugging more difficult.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree with deleting this handler. Notice that OCaml stack traces shoud remain understandable here: signaling that the exception is "re-raised".

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I was being overly pedantic here. While stack trace preservation is somewhat heuristic and not guaranteed in all scenarios, the compiler should be smart enough in this particular case, as you correctly point out.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants