From 003e35a0080d46ccc705eb658754fac46b4bd0f5 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 17 Dec 2020 17:53:48 +0100
Subject: [PATCH] Add first support for detection of solvers. Also rework
verify command semantics.
---
dune | 4 +-
main.ml | 106 +++++++++++++-------
solver.ml | 278 +++++++++++++++++++++++++++++++++++++----------------
solver.mli | 20 +++-
4 files changed, 289 insertions(+), 119 deletions(-)
diff --git a/dune b/dune
index acf23b2a..a29ce3f4 100644
--- a/dune
+++ b/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)))
diff --git a/main.ml b/main.ml
index 3f2da3a8..4c184336 100644
--- a/main.ml
+++ b/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)
diff --git a/solver.ml b/solver.ml
index 3c0796d3..7ab738ba 100644
--- a/solver.ml
+++ b/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;
diff --git a/solver.mli b/solver.mli
index e85cb9cb..33c86da5 100644
--- a/solver.mli
+++ b/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
--
GitLab