Add first support for detection of solvers. Also rework verify command semantics.

dune

@@ -8,5 +8,5 @@
   (name main)
   (public_name caisar)
   (modules_without_implementation property_syntax)
-  (libraries cmdliner logs logs.cli logs.fmt fmt.tty base unix str)
-  (preprocess (pps ppx_deriving.show ppx_deriving.ord)))
+  (libraries yojson cmdliner logs logs.cli logs.fmt fmt.tty base unix str ppx_deriving_yojson.runtime)
+  (preprocess (pps ppx_deriving_yojson ppx_deriving.show ppx_deriving.ord)))

main.ml

@@ -8,6 +8,8 @@ open Base
 open Cmdliner
 module Format = Caml.Format
 
+let caisar = "caisar"
+
 
 (* Logs. *)
 
@@ -43,16 +45,28 @@ let setup_logs =
 
 (* Commands. *)
 
-let verify cmd model property solver raw_options () =
+let config cmd detect force filename () =
+  Logs.debug
+    (fun m -> m "Command `%s' with configuration file `%s'."
+        cmd filename);
+  if detect
+  then begin
+    match Solver.detect ~force filename with
+    | Ok () -> Logs.app (fun m -> m "Configuration saved in `%s'." filename)
+    | Error e -> Logs.err (fun m -> m "%s" e)
+  end
+
+let verify cmd raw_options config model property solver () =
   Logs.debug
     (fun m ->
        m "Command `%s' with@ model `%s',@ property `%s' and@ solver `%s'."
-         cmd model property (Solver.show_solver solver));
+         cmd model property solver);
   let do_verify () =
     let open Result in
     Model.build ~filename:model >>= fun model ->
     Property.build ~filename:property >>= fun property ->
-    Solver.exec ?raw_options solver model property
+    Solver.config_solver ~solver config >>= fun config_solver ->
+    Solver.exec ?raw_options config_solver model property
   in
   match do_verify () with
   | Ok () -> Logs.app (fun m -> m "Done.")
@@ -61,63 +75,87 @@ let verify cmd model property solver raw_options () =
 
 (* Command line. *)
 
+let config_cmd =
+  let cmdname = "config" in
+  let detect =
+    let doc = Format.sprintf "Detect (supported) solvers in \\$PATH." in
+    Arg.(value & flag & info ["d"; "detect"] ~doc)
+  in
+  let filename =
+    let docv_filename = "FILE" in
+    let doc =
+      Format.sprintf "$(b,FILE) to write the %s configuration to." caisar
+    in
+    Arg.(value & pos 0 file Solver.default_config_filename
+         & info [] ~docv:docv_filename ~doc)
+  in
+  let force =
+    let doc = "Force creation of configuration $(b,FILE)." in
+    Arg.(value & flag & info ["f"; "force-create"] ~doc)
+  in
+  let doc = Format.sprintf "%s configuration." caisar in
+  let exits = Term.default_exits in
+  let man = [
+    `S Manpage.s_description;
+    `P (Format.sprintf "Handle the configuration of %s." caisar); ]
+  in
+  let envs =
+    List.map
+      ~f:(Term.env_info
+            ~doc:"Use $(env) to specify the respective executable directory.")
+      Solver.env_vars
+  in
+  Term.(ret
+          (const (fun cmdname detect force filename _ ->
+               if not detect
+               then `Help (`Pager, Some "config")
+               else `Ok (config cmdname detect force filename ()))
+           $ const cmdname $ detect $ force $ filename $ setup_logs)),
+  Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man
+
 let verify_cmd =
   let cmdname = "verify" in
   let docv_solver = "SOLVER" in
   let solver =
-    let doc =
-      let solvers =
-        List.map
-          ~f:(fun s -> String.lowercase (Solver.show_solver s))
-          (* TODO: This should be computed dynamically. *)
-          [ Solver.Marabou; Solver.Pyrat ]
-      in
-      let doc_alts = Arg.doc_alts solvers in
-      Format.sprintf
-        "The solver to use for verification. $(docv) must be %s."
-        doc_alts
-    in
-    let conv_solver =
-      Arg.enum [ ("pyrat", Solver.Pyrat); ("marabou", Solver.Marabou); ]
-    in
-    let default_solver = Solver.Marabou in
-    Arg.(value
-         & pos 2 conv_solver default_solver
+    let doc = "The solver to use for verification." in
+    Arg.(required
+         & pos 2 (some string) None
          & info [] ~docv:docv_solver ~doc)
   in
   let docv_model = "MODEL" in
   let model =
-    let doc = "The $(b,filename) of a neural network model." in
+    let doc = "$(b,FILE) of a neural network model." in
     Arg.(required & pos 0 (some file) None & info [] ~docv:docv_model ~doc)
   in
   let docv_property = "PROPERTY" in
   let property =
-    let doc = "The $(b,filename) of a property to verify." in
+    let doc = "$(b,FILE) of a property to verify." in
     Arg.(required & pos 1 (some file) None & info [] ~docv:docv_property ~doc)
   in
   let solver_raw_options =
     let doc = "Additional options provided to the solver." in
     Arg.(value & opt (some string) None & info ["raw"; "raw-options"] ~doc)
   in
+  let config_filename =
+    let doc = "$(b,FILE) to read the configuration from." in
+    Arg.(value & opt file Solver.default_config_filename
+         & info ["c"; "config"] ~doc)
+  in
   let doc = "Property verification of neural networks." in
   let exits = Term.default_exits in
   let man = [
     `S Manpage.s_description;
     `P (Format.sprintf
-          "Verifies $(i,%s) on $(i,%s) by using $(i,%s)."
+          "Verify $(i,%s) on $(i,%s) by using $(i,%s)."
           docv_property docv_model docv_solver); ]
   in
-  let envs =
-    List.map
-      ~f:(Term.env_info
-            ~doc:"Use value of $(env) as the respective executable.")
-      Solver.env_vars
-  in
   Term.(const verify
         $ const cmdname
+        $ solver_raw_options
+        $ config_filename
         $ model $ property $ solver
-        $ solver_raw_options $ setup_logs),
-  Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man
+        $ setup_logs),
+  Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man
 
 let default_cmd =
   let doc = "Framework for neural networks property verification and more." in
@@ -132,9 +170,9 @@ let default_cmd =
   in
   let version = "0.0" in
   Term.(ret (const (fun _ -> `Help (`Pager, None)) $ const ())),
-  Term.info "caisar" ~version ~doc ~sdocs ~exits:Term.default_exits ~man
+  Term.info caisar ~version ~doc ~sdocs ~exits:Term.default_exits ~man
 
 let () =
-  match Term.(eval_choice default_cmd [ verify_cmd ]) with
+  match Term.(eval_choice default_cmd [ verify_cmd; config_cmd ]) with
   | `Error _ -> Caml.exit 1
   | _ -> Caml.exit (if Logs.err_count () > 0 then 1 else 0)

solver.ml

@@ -8,10 +8,16 @@ open Base
 module Format = Caml.Format
 module Sys = Caml.Sys
 
+(* Supported solvers. *)
 type solver =
   | Pyrat
   | Marabou
- [@@deriving show { with_path = false }]
+ [@@deriving show { with_path = false }, yojson]
+
+
+(* Utilities. *)
+
+let defaults = [ Pyrat; Marabou ]
 
 let rec pp_property_marabou property =
   let open Property_syntax in
@@ -43,8 +49,8 @@ let pp_property solver property =
   | Marabou ->
     Ok (pp_property_marabou property)
 
-let env_var_of_solver solver = String.uppercase (show_solver solver ^ "_exe")
-let env_vars = List.map ~f:env_var_of_solver [ Pyrat; Marabou ]
+let env_var_of_solver solver = String.uppercase (show_solver solver ^ "_dir")
+let env_vars = List.map ~f:env_var_of_solver defaults
 
 let default_exe_name_of_solver = function
   | Pyrat -> "pyrat.py"
@@ -55,25 +61,15 @@ let default_option_of_solver = function
   | Marabou -> "--version"
 
 let exe_name_of_solver solver =
+  let exe = default_exe_name_of_solver solver in
   match Sys.getenv_opt (env_var_of_solver solver) with
-  | None -> default_exe_name_of_solver solver
-  | Some v -> v
+  | None -> exe
+  | Some v -> v ^ exe
 
-let default_exec_of_solver solver =
-  let module Filename = Caml.Filename in
-  let tmp = Filename.temp_file "caisar" "" in
-  let cmd =
-    Filename.quote_command
-      ~stdout:tmp ~stderr:tmp
-      (exe_name_of_solver solver)
-      [default_option_of_solver solver]
-  in
-  let retcode = Sys.command cmd in
-  let in_channel = Stdlib.open_in tmp in
-  let firstline = Stdlib.input_line in_channel in
-  Stdlib.close_in in_channel;
-  Sys.remove tmp;
-  cmd, retcode, firstline
+
+(* Configuration. *)
+
+type version = [`Unknown_version | `Version of string] [@@deriving yojson, show]
 
 let version_of_solver solver s =
   let regexp_string =
@@ -86,41 +82,154 @@ let version_of_solver solver s =
   let regexp_version = Str.regexp regexp_string in
   try
     ignore (Str.search_forward regexp_version s 0);
-    Ok (Str.matched_string s)
+    `Version (Str.matched_string s)
   with Stdlib.Not_found ->
-    Error "No recognizable version found."
+    Logs.debug (fun m -> m "No recognizable version found.");
+    `Unknown_version
+
+
+type config_solver = {
+  name: string;
+  solver: solver;
+  exe: string;
+  version: version;
+} [@@deriving yojson]
+
+type config = config_solver list [@@deriving yojson]
+
+let default_config_filename =
+  let filename = ".caisar.conf" in
+  match Sys.getenv_opt "HOME" with
+  | None -> filename
+  | Some p -> p ^ "/.caisar.conf"
+
+let out_channel_of_config_filename ~force filename =
+  if force || not (Sys.file_exists filename)
+  then begin
+    Logs.debug (fun m -> m "Creating configuration file `%s'." filename);
+    Ok (Stdlib.open_out filename)
+  end
+  else
+    Error (Format.sprintf "Configuration file `%s' already exists." filename)
+
+let detect ~force filename =
+  let open Result in
+  let module Filename = Caml.Filename in
+  Logs.info (fun m ->
+      m "Detecting%s solvers in \\$PATH, and writing configuration file `%s'."
+        (if force then " (force)" else "") filename);
+  (* Create the configuration file. *)
+  out_channel_of_config_filename ~force filename >>= fun out_channel ->
+  (* Build a [config_solver] for each supported solver. *)
+  try
+    let config =
+      List.filter_map
+        ~f:(fun solver ->
+            (* We detect whether solver is available in PATH, or in the provided
+               path via env variable, by executing `solver --version' command. *)
+            let tmp = Filename.temp_file "caisar" "detect" in
+            let exe = exe_name_of_solver solver in
+            let cmd =
+              Filename.quote_command
+                ~stdout:tmp ~stderr:tmp
+                exe
+                [default_option_of_solver solver]
+            in
+            let retcode = Sys.command cmd in
+            let in_channel = Stdlib.open_in tmp in
+            let firstline = Stdlib.input_line in_channel in
+            Stdlib.close_in in_channel;
+            Sys.remove tmp;
+            let solver_name = show_solver solver in
+            if retcode <> 0
+            then begin
+              Logs.info (fun m -> m "No solver `%s' found." solver_name);
+              None
+            end
+            else begin
+              (* If available, we save build a [config_solver] for solver. *)
+              let version = version_of_solver solver firstline in
+              let config_solver =
+                { name = String.lowercase solver_name;
+                  solver;
+                  exe;
+                  version; }
+              in
+              Logs.app
+                (fun m -> m "Found solver `%s': %s."
+                    solver_name (show_version version));
+              Some config_solver
+            end)
+        defaults
+    in
+    Logs.app (fun m -> m "%d solver(s) added." (List.length config));
+    (* We write all solver configs in the configuration file, as JSON data. *)
+    let config_json = config_to_yojson config in
+    Yojson.Safe.pretty_to_channel out_channel config_json;
+    Ok ()
+  with _ ->
+    Error "Unexpected failure."
+
+let config_solver ~solver filename =
+  let open Result in
+  Logs.info
+    (fun m -> m "Reading configuration file `%s' for solver `%s'."
+        filename solver);
+  if not (Sys.file_exists filename)
+  then Error (Format.sprintf "Configuration file `%s' not exist." filename)
+  else begin
+    (* Read all solver configs present in the given configuration file. *)
+    config_of_yojson (Yojson.Safe.from_file filename) >>= fun config ->
+    (* Search for a [config_solver] with a name [solver]. *)
+    match List.find ~f:(fun cs -> String.equal cs.name solver) config with
+    | None ->
+      Error
+        (Format.sprintf
+           "No solver with name `%s' found in configuration file `%s'."
+           solver filename)
+    | Some config_solver ->
+      begin
+        Logs.info
+          (fun m -> m "Found `%s' `%s'."
+              (show_solver config_solver.solver)
+              (show_version config_solver.version));
+        Ok config_solver
+      end
+  end
+
+
+(* Verification. *)
 
-let check_availability ~err_on_version_mismatch solver =
-  let solver_name = show_solver solver in
+let check_availability config_solver =
+  let module Filename = Caml.Filename in
+  let solver_name = config_solver.name in
   Logs.info (fun m -> m "Checking availability of `%s'." solver_name);
   try
-    let cmd, retcode, firstline = default_exec_of_solver solver in
-    if retcode <> 0
+    (* Execute command `solver --version' to check actual availability. *)
+    let tmp = Filename.temp_file "caisar" "avail" in
+    let cmd =
+      Filename.quote_command
+        ~stdout:tmp ~stderr:tmp
+        config_solver.exe
+        [default_option_of_solver config_solver.solver]
+    in
+    let retcode = Sys.command cmd in
+    let in_channel = Stdlib.open_in tmp in
+    Stdlib.close_in in_channel;
+    Sys.remove tmp;
+    if retcode = 0
     then
+      Ok ()
+    else
       Error
         (Format.sprintf
-           "Command `%s' failed.@ \
-            Hint: Set either the PATH or \
-            use variable `%s' to directly provide the path to the executable."
-           cmd (env_var_of_solver solver))
-    else begin
-      match version_of_solver solver firstline with
-      | Error _ as error ->
-        if err_on_version_mismatch
-        then error
-        else begin
-          Logs.warn
-            (fun m -> m "Found unrecognizable version of `%s'." solver_name);
-          Ok ()
-        end
-      | Ok version ->
-        Logs.info (fun m -> m "Found version `%s'." version);
-        Ok ()
-    end
-  with Stdlib.Not_found | End_of_file | Sys_error _ ->
+           "Command `%s' failed. Try to launch the configuration process again."
+           cmd)
+  with Stdlib.Not_found | End_of_file | Failure _ | Sys_error _ ->
     Error "Unexpected failure."
 
-let check_compatibility solver model =
+let check_compatibility config_solver model =
+  let solver = config_solver.solver in
   match solver, model.Model.format with
   | (Pyrat | Marabou), (Model.Onnx as f) ->
     Error
@@ -131,9 +240,10 @@ let check_compatibility solver model =
   | _ ->
     Ok ()
 
-let build_command ?raw_options solver property model =
+let build_command ?raw_options confg_solver property model =
   let module Filename = Caml.Filename in
   let open Result in
+  let solver = confg_solver.solver in
   (* Format property wrt solver. *)
   pp_property solver property >>= fun s ->
   (* Write property to temporary file. *)
@@ -149,49 +259,53 @@ let build_command ?raw_options solver property model =
       Error (Format.sprintf "Unexpected failure@ `%s'." e)
   end >>= fun prop ->
   (* Build actual command-line. *)
-  let cmd =
-    let raw_options = Option.to_list raw_options in
-    match solver with
-    | Pyrat ->
-      let verbose =
-        match Logs.level () with
-        | None | Some (App | Error | Warning) -> false
-        | Some (Info | Debug) -> true
-      in
-      Filename.quote_command
-        (exe_name_of_solver solver)
-        (model.Model.filename ::
-         prop ::
-         if verbose then "--verbose" :: raw_options else raw_options)
-    | Marabou ->
-      let verbosity_level =
-        match Logs.level () with
-        | None | Some (App | Error | Warning) -> 0
-        | Some Info -> 1
-        | Some Debug -> 2
-      in
-      Filename.quote_command
-        (exe_name_of_solver solver)
-        ("--property" ::  prop ::
-         "--input" :: model.Model.filename ::
-         "--verbosity" :: Int.to_string verbosity_level ::
-         raw_options)
-  in
-  Ok (prop, cmd)
+  try
+    let cmd =
+      let raw_options = Option.to_list raw_options in
+      let exe = confg_solver.exe in
+      match solver with
+      | Pyrat ->
+        let verbose =
+          match Logs.level () with
+          | None | Some (App | Error | Warning) -> false
+          | Some (Info | Debug) -> true
+        in
+        Filename.quote_command
+          exe
+          (model.Model.filename ::
+           prop ::
+           if verbose then "--verbose" :: raw_options else raw_options)
+      | Marabou ->
+        let verbosity_level =
+          match Logs.level () with
+          | None | Some (App | Error | Warning) -> 0
+          | Some Info -> 1
+          | Some Debug -> 2
+        in
+        Filename.quote_command
+          exe
+          ("--property" ::  prop ::
+           "--input" :: model.Model.filename ::
+           "--verbosity" :: Int.to_string verbosity_level ::
+           raw_options)
+    in
+    Ok (prop, cmd)
+  with Failure e ->
+    Error (Format.sprintf "Unexpected failure@ `%s'." e)
 
-let exec ?raw_options solver model property =
+let exec ?raw_options config_solver model property =
   let open Result in
-  (* Check solver availability in PATH. *)
-  check_availability ~err_on_version_mismatch:false solver >>= fun () ->
+  (* Check solver availability. *)
+  check_availability config_solver >>= fun () ->
   (* Check solver and model compatibility. *)
-  check_compatibility solver model >>= fun () ->
+  check_compatibility config_solver model >>= fun () ->
   (* Build the required command-line. *)
-  build_command ?raw_options solver property model >>= fun (tmp, cmd) ->
+  build_command ?raw_options config_solver property model >>= fun (tmp, cmd) ->
   (* Execute the command. *)
   begin
     try
       Logs.app
-        (fun m -> m "Launching verification with `%s'." (show_solver solver));
+        (fun m -> m "Launching verification with `%s'." config_solver.name);
       Logs.debug (fun m -> m "Executing command `%s'." cmd);
       let retcode = Sys.command cmd in
       Sys.remove tmp;

solver.mli

@@ -7,10 +7,28 @@
 (** Supported solvers. *)
 type solver = Pyrat | Marabou [@@deriving show]
 
+(** The list of supported solvers by default. *)
+val defaults: solver list
+
 val env_vars: string list
 
+val default_config_filename: string
+
+(** [detect ~force file] searches for solvers in $PATH, or in the paths provided
+    via [env_vars], and save the configurations in [file].
+    By default, it does not overwrite [file] if it already exists.
+    @param force if true, forces the creation of [file]. *)
+val detect: force:bool -> string -> (unit, string) Result.t
+
+(** Solver configuration. *)
+type config_solver
+
+(** [config_solver ~solver file] retrieves the [solver] configuration, if any,
+    from the given [file]. *)
+val config_solver: solver:string -> string -> (config_solver, string) Result.t
+
 (** [exec ?raw_options solver model property] runs [solver] on [property] for
     [model] with the provided [raw_options], if any. *)
 val exec:
   ?raw_options:string ->
-  solver -> Model.t -> Property.t -> (unit, string) Result.t
+  config_solver -> Model.t -> Property.t -> (unit, string) Result.t