Add --from-file argument to run command

Allow specifying a list of files to run through the command line
argument `--from-file|-F`.

Also uses cmdliner's `file` parser to parse valid Fpath's

bench/runner/multi_query.ml

@@ -63,7 +63,7 @@ let write_data_frame started_at results_dir (prover, df) =
   let csv_path = Fpath.(results_dir / csv_file) in
   Owl_dataframe.to_csv ~sep:',' df (Fpath.to_string csv_path)
 
-let main _hook provers dirs =
+let main _hook provers from_file dirs =
   let open Result in
   let now = Core_unix.(localtime @@ gettimeofday ()) in
   let started_at = Core_unix.strftime now "%Y%m%dT%H%M%S" in
@@ -76,7 +76,7 @@ let main _hook provers dirs =
     List.map
       (fun p ->
         let ((status, stdout, _stderr, _) as result) =
-          Tool.fork_and_run p dirs
+          Tool.fork_and_run ?from_file p dirs
         in
         Fmt.pr "@[<v 2>Run %a@;Exited: %a@;Stdout:@; %a@]@." Tool.pp_prover p
           pp_exit_status status Fmt.string (String.escaped stdout);

bench/runner/runner.ml

@@ -14,13 +14,16 @@ let cli =
   let dirs = Arg.(value & pos_all fpath_dir [] & info [] ~docv:"PATH") in
   let provers = Arg.(value & opt_all prover_conv [] & info [ "p"; "prover" ]) in
   let timeout = Arg.(value & opt (some int) None & info [ "timeout" ]) in
+  let from_file =
+    Arg.(value & opt (some file) None & info [ "F"; "from-file" ])
+  in
   let single_query =
     let info = Cmd.info "single-query" in
     Cmd.v info Term.(const Single_query.main $ hook $ provers $ timeout $ dirs)
   in
   let multi_query =
     let info = Cmd.info "multi-query" in
-    Cmd.v info Term.(const Multi_query.main $ hook $ provers $ dirs)
+    Cmd.v info Term.(const Multi_query.main $ hook $ provers $ from_file $ dirs)
   in
   let info = Cmd.info "runner" in
   Cmd.group info [ single_query; multi_query ]

bench/runner/tool.ml

@@ -43,15 +43,18 @@ let is_available = function
     Smtml.Solver_dispatcher.is_available Colibri2_solver
   | Smtml { name = Z3; _ } -> Smtml.Solver_dispatcher.is_available Z3_solver
 
-let cmd prover files =
+let cmd ?from_file prover files =
   match prover with
   | Z3 -> ("z3", "z3" :: files)
   | Smtml { name; st } ->
     ( "smtml"
     , let args =
         "--mode" :: "incremental" :: "--solver"
         :: Fmt.str "%a" pp_prover_name name
-        :: files
+        ::
+        ( match from_file with
+        | None -> files
+        | Some file -> "--from-file" :: [ file ] )
       in
       "smtml" :: "run" :: (if st then "--print-statistics" :: args else args) )
 
@@ -68,10 +71,10 @@ let with_ic fd f =
   let ic = Unix.in_channel_of_descr fd in
   Fun.protect ~finally:(fun () -> In_channel.close ic) (fun () -> f ic)
 
-let fork_and_run ?timeout prover file =
+let fork_and_run ?timeout ?from_file prover file =
   let stdout_read, stdout_write = Unix.pipe ~close_on_exec:false () in
   let stderr_read, stderr_write = Unix.pipe ~close_on_exec:false () in
-  let prog, argv = cmd prover file in
+  let prog, argv = cmd ?from_file prover file in
   let pid =
     Unix.fork_exec ~prog ~argv () ~preexec_fn:(fun () ->
         Unix.close stdout_read;

bin/main.ml

@@ -28,7 +28,23 @@ let get_solver debug solver prover_mode =
   | Cached -> (module Solver.Cached (Mappings))
   | Incremental -> (module Solver.Incremental (Mappings))
 
-let run debug solver prover_mode dry print_statistics files =
+(* FIXME: this function has a sad name *)
+let parse_file filename =
+  let open Smtml_prelude.Result in
+  let+ lines = Bos.OS.File.read_lines filename in
+  (* FIXME: this can be improved *)
+  let files =
+    List.fold_left
+      (fun acc line ->
+        let line = String.trim line in
+        (* Assume '#' at the start of a line is a comment *)
+        if String.starts_with ~prefix:"#" line then acc else Fpath.v line :: acc
+        )
+      [] lines
+  in
+  List.rev files
+
+let run debug solver prover_mode dry print_statistics from_file files =
   if debug then Logs.Src.set_level Log.src (Some Logs.Debug);
   Logs.set_reporter @@ Logs.format_reporter ();
   let module Solver = (val get_solver debug solver prover_mode) in
@@ -84,7 +100,16 @@ let run debug solver prover_mode dry print_statistics files =
         Log.err (fun k -> k "%s" err);
         prev_state )
   in
-  let _ = List.fold_left run_path None files in
+  let _ =
+    match from_file with
+    | None -> List.fold_left run_path None files
+    | Some file -> (
+      match parse_file file with
+      | Error (`Msg err) ->
+        Log.err (fun k -> k "%s" err);
+        None
+      | Ok files -> List.fold_left run_file None files )
+  in
   if print_statistics then Log.app (fun k -> k "total time: %.06f" !total_t);
   let write_exception_log = function
     | [] -> Ok ()

bin/options.ml

@@ -14,7 +14,15 @@ let prove_mode_conv =
   Cmdliner.Arg.enum
     [ ("batch", Batch); ("cached", Cached); ("incremental", Incremental) ]
 
-let path = ((fun s -> `Ok (Fpath.v s)), Fpath.pp)
+let path =
+  let parser, _ = Cmdliner.Arg.file in
+  ( (fun file ->
+      if String.equal "-" file then `Ok (Fpath.v file)
+      else
+        match parser file with
+        | `Ok file -> `Ok (Fpath.v file)
+        | `Error _ as err -> err )
+  , Fpath.pp )
 
 let file0 =
   let doc = "Input file" in
@@ -46,12 +54,20 @@ let print_statistics =
   let doc = "Print statistics" in
   Arg.(value & flag & info [ "print-statistics" ] ~doc)
 
+let from_file =
+  let doc =
+    "File containing a list of files to run. This argument discards any \
+     positional arguments provided."
+  in
+  Arg.(value & opt (some path) None & info [ "F"; "from-file" ] ~doc ~docv:"VAL")
+
 let cmd_run f =
   let doc = "Runs one or more scripts using. Also supports directory inputs" in
   let info = Cmd.info "run" ~doc in
   Cmd.v info
     Term.(
-      const f $ debug $ solver $ solver_mode $ dry $ print_statistics $ files )
+      const f $ debug $ solver $ solver_mode $ dry $ print_statistics
+      $ from_file $ files )
 
 let cmd_to_smt2 f =
   let doc = "Convert .smtml into .smt2" in

test/smt2/test_smt2.t

@@ -1,6 +1,9 @@
 Test parsing a nonexistent file:
   $ smtml run idontexist.smt2
-  smtml: [WARNING] idontexist.smt2: No such file or directory
+  smtml: FILES… arguments: no 'idontexist.smt2' file or directory
+  Usage: smtml run [OPTION]… [FILES]…
+  Try 'smtml run --help' or 'smtml --help' for more information.
+  [2]
 
 Test parsing an empty file:
   $ smtml run test_empty.smt2
@@ -50,3 +53,32 @@ Test BitVector parsing:
 Test FloatingPoint parsing:
   $ smtml run test_fp.smt2
   sat
+
+Tests smt2 with the --from-file argument:
+  $ cat <<EOF > test.list
+  > test_empty.smt2
+  > test_core_all.smt2
+  > test_lia.smt2
+  > test_lra.smt2
+  > test_fp.smt2
+  > test_string_all.smt2
+  > EOF
+  $ smtml run --from-file test.list
+  sat
+  sat
+  (model
+    (w false)
+    (x true)
+    (y true)
+    (z true))
+  sat
+  sat
+  sat
+  (model
+    (x -2.)
+    (y 4.))
+  sat
+  sat
+  (model
+    (x "abcd")
+    (y "a"))