diff --git a/dune b/dune
index a29ce3f422f3715c9df5320baa6691f5598391ab..2bc8efeaadff54275c498c99f041fd8c70f8d0ba 100644
--- a/dune
+++ b/dune
@@ -9,4 +9,4 @@
(public_name caisar)
(modules_without_implementation property_syntax)
(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)))
+ (preprocess (pps ppx_deriving_yojson ppx_deriving.show ppx_deriving.ord ppx_deriving.eq)))
diff --git a/main.ml b/main.ml
index cf118bd9873db493f21b2da5d0089733775b58bf..1384273d645244c11c3434927b72a9843e18a4a1 100644
--- a/main.ml
+++ b/main.ml
@@ -45,30 +45,29 @@ let setup_logs =
(* Commands. *)
-let config cmd detect filename () =
- let filename = Option.value filename ~default:Solver.default_config_filename in
+let config cmd detect file_opt () =
+ let file = Option.value file_opt ~default:Solver.default_config_file in
Logs.debug
- (fun m -> m "Command `%s' with configuration file `%s'."
- cmd filename);
+ (fun m -> m "Command `%s' with configuration file `%s'." cmd file);
if detect
then begin
- match Solver.detect filename with
- | Ok () -> Logs.app (fun m -> m "Configuration saved in `%s'." filename)
+ match Solver.detect ~file with
+ | Ok () -> Logs.app (fun m -> m "Configuration saved in `%s'." file)
| Error e -> Logs.err (fun m -> m "%s" e)
end
-let verify cmd raw_options config model property solver () =
+let verify cmd raw_options config_file model property solver () =
Logs.debug
(fun m ->
m "Command `%s' with@ model `%s',@ property `%s' and@ solver `%s' \
(using configuration file `%s')."
- cmd model property solver config);
+ cmd model property (Solver.show_solver solver) config_file);
let do_verify () =
let open Result in
Model.build ~filename:model >>= fun model ->
Property.build ~filename:property >>= fun property ->
- Solver.get_config_solver ~solver config >>= fun config_solver ->
- Solver.exec ?raw_options config_solver model property
+ Solver.get_config solver ~file:config_file >>= fun config ->
+ Solver.exec ?raw_options config model property
in
match do_verify () with
| Ok () -> Logs.app (fun m -> m "Done.")
@@ -79,8 +78,16 @@ let verify cmd raw_options config model property solver () =
let config_cmd =
let cmdname = "config" in
+ let dirvar = "DIR" in
+ let envs =
+ [ Term.env_info
+ ~doc:"Path to directory where to search for the executable of a solver."
+ dirvar ]
+ in
let detect =
- let doc = Format.sprintf "Detect (supported) solvers in \\$PATH." in
+ let doc =
+ Format.sprintf "Detect solvers in \\$PATH (or \\$%s, if specified)." dirvar
+ in
Arg.(value & flag & info ["d"; "detect"] ~doc)
in
let filename =
@@ -97,12 +104,6 @@ let config_cmd =
`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 filename _ ->
if not detect && Option.is_none filename
@@ -117,9 +118,18 @@ let verify_cmd =
let cmdname = "verify" in
let docv_solver = "SOLVER" in
let solver =
- let doc = "The solver to use for verification." in
+ let doc =
+ "The solver to use for verification. \
+ $(docv) must be either `pyrat' or `marabou'."
+ in
+ let solvers =
+ Arg.enum
+ (List.map
+ ~f:(fun s -> String.lowercase (Solver.show_solver s), s)
+ Solver.defaults)
+ in
Arg.(required
- & pos 2 (some string) None
+ & pos 2 (some solvers) (Some Solver.Pyrat)
& info [] ~docv:docv_solver ~doc)
in
let docv_model = "MODEL" in
@@ -138,7 +148,7 @@ let verify_cmd =
in
let config_filename =
let doc = "$(b,FILE) to read the configuration from." in
- Arg.(value & opt file Solver.default_config_filename
+ Arg.(value & opt file Solver.default_config_file
& info ["c"; "config"] ~doc)
in
let doc = "Property verification of neural networks." in
diff --git a/solver.ml b/solver.ml
index d31c2df48dfbf7090d953f51106b5152a217e861..5078ddbe4d9a78703a22cc2b3729403bd43a667f 100644
--- a/solver.ml
+++ b/solver.ml
@@ -12,7 +12,7 @@ module Sys = Caml.Sys
type solver =
| Pyrat
| Marabou
- [@@deriving show { with_path = false }, yojson]
+ [@@deriving show { with_path = false }, ord, eq, yojson]
(* Utilities. *)
@@ -51,9 +51,6 @@ let pp_property solver property =
| Marabou ->
Ok (pp_property_marabou property)
-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"
| Marabou -> "Marabou"
@@ -64,7 +61,7 @@ let default_option_of_solver = function
let exe_path_of_solver solver =
let exe = default_exe_name_of_solver solver in
- match Sys.getenv_opt (env_var_of_solver solver) with
+ match Sys.getenv_opt "DIR" with
| None ->
begin
(* We want the complete path of [exe] in $PATH: we use `command -v [exe]'
@@ -91,7 +88,17 @@ let exe_path_of_solver solver =
(* Configuration. *)
type version =
- [`Unknown_version | `Version of string] [@@deriving yojson, show]
+ | Unknown
+ | Version of string
+[@@deriving show { with_path = false }, yojson]
+
+type config = {
+ solver: solver;
+ exe: string;
+ version: version;
+} [@@deriving yojson, show]
+
+type full_config = config list [@@deriving yojson, show]
let version_of_solver solver s =
let regexp_string =
@@ -104,66 +111,62 @@ let version_of_solver solver s =
let regexp_version = Str.regexp regexp_string in
try
ignore (Str.search_forward regexp_version s 0);
- `Version (Str.matched_string s)
+ Version (Str.matched_string s)
with Stdlib.Not_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]
+ Unknown
-type config = config_solver list [@@deriving yojson]
-
-let default_config_filename =
+let default_config_file =
let filename = ".caisar.conf" in
match Sys.getenv_opt "HOME" with
| None -> filename
| Some p -> p ^ "/.caisar.conf"
-let get_config filename =
- try config_of_yojson (Yojson.Safe.from_file filename)
- with Yojson.Json_error e -> Error e
+let get_full_config filename =
+ let open Result in
+ match full_config_of_yojson (Yojson.Safe.from_file filename) with
+ | Error _ | exception _ ->
+ []
+ | Ok full_config ->
+ begin
+ Logs.debug
+ (fun m -> m "Configuration in file `%s':@ %s"
+ filename (show_full_config full_config));
+ full_config
+ end
-let get_config_solver ~solver filename =
+let get_config ~file solver =
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)
+ (fun m -> m "Reading configuration file `%s' for solver `%a'."
+ file
+ pp_solver solver);
+ if not (Sys.file_exists file)
+ then Error (Format.sprintf "Configuration file `%s' not exist." file)
else begin
(* Read all solver configs present in the given configuration file. *)
- get_config 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
+ let full_config = get_full_config file in
+ (* Search for a [config] with [solver]. *)
+ match List.find ~f:(fun cs -> equal_solver cs.solver solver) full_config with
| None ->
Error
- (Format.sprintf
- "No solver with name `%s' found in configuration file `%s'."
- solver filename)
- | Some config_solver ->
+ (Format.asprintf
+ "No solver `%a' found in configuration file `%s'."
+ pp_solver solver
+ file)
+ | Some config ->
begin
Logs.info
- (fun m -> m "Found `%s' `%s'."
- (show_solver config_solver.solver)
- (show_version config_solver.version));
- Ok config_solver
+ (fun m -> m "Found `%a' `%s'."
+ pp_solver config.solver
+ (show_version config.version));
+ Ok config
end
end
-let create_config_file filename =
- Logs.debug (fun m -> m "Creating configuration file `%s'." filename);
- let config =
- if Sys.file_exists filename
- then Some (get_config filename)
- else None
- in
- Stdlib.open_out filename, config
+let create_config_file file =
+ Logs.debug (fun m -> m "Creating new configuration file `%s'." file);
+ Stdlib.open_out file
let detect_default_solvers () =
let module Filename = Caml.Filename in
@@ -182,30 +185,29 @@ let detect_default_solvers () =
exe
[default_option_of_solver solver]
in
+ Logs.debug
+ (fun m -> m "Executing command `%s' to detect `%a'."
+ cmd pp_solver solver);
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);
+ Logs.info (fun m -> m "No solver `%a' found." pp_solver solver);
None
end
else begin
- (* If available, we save build a [config_solver] for solver. *)
+ (* If available, we save a [config] for solver. *)
let version = version_of_solver solver firstline in
- let config_solver =
- { name = String.lowercase solver_name;
- solver;
- exe;
- version; }
- in
+ let config = { solver; exe; version; } in
Logs.app
- (fun m -> m "Found solver `%s' (%s): %s."
- solver_name exe (show_version version));
- Some config_solver
+ (fun m -> m "Found solver `%a' `%a' (%s)."
+ pp_solver solver
+ pp_version version
+ exe);
+ Some config
end)
defaults
in
@@ -213,54 +215,50 @@ let detect_default_solvers () =
with _ ->
Error "Unexpected failure."
-
-let detect filename =
+let detect ~file =
let open Result in
- Logs.info (fun m ->
- m "Detecting solvers and writing configuration file `%s'."
- filename);
- (* Create new configuration file and retrieve the `config' from the existing
- one, if any. *)
- let out_channel, config_opt = create_config_file filename in
- (* Detect default supported solvers in $PATH. *)
- detect_default_solvers () >>= fun default_config ->
- (* Build [config] by first appending [default_config] and the existing one
- [config_opt], and then deduping the result. *)
- begin
- match config_opt with
- | None ->
- Ok default_config
- | Some or_config ->
- or_config >>= fun current_config ->
- (* We consider two solvers equal as soon as their `name' is. *)
- (* TODO: This comparison is not optimal but needed as long as we register
- solver names as lazily as done in [detect_default_solvers]. *)
- let compare cs1 cs2 = String.compare cs1.name cs2.name in
- Ok
- (List.dedup_and_sort
- ~compare
- (List.append current_config default_config))
- end >>= fun config ->
+ (* Retrieve the current configuration from [file]. *)
+ let current_full_config = get_full_config file in
+ (* Create new configuration file. *)
+ let out_channel = create_config_file file in
+ (* Detect default supported solvers in $PATH or $DIR. *)
+ detect_default_solvers () >>= fun default_full_config ->
+ (* Build [full_config] by first appending [default_full_config] to
+ [current_full_config], and then deduping the result. *)
+ let full_config =
+ (* TODO: This comparison is not optimal but sufficient as long as we register
+ solver as simply as done in [detect_default_solvers]. *)
+ let compare cs1 cs2 = compare_solver cs1.solver cs2.solver in
+ List.dedup_and_sort
+ ~compare
+ (List.append current_full_config default_full_config)
+ in
(* 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;
+ let full_config_json = full_config_to_yojson full_config in
+ Yojson.Safe.pretty_to_channel out_channel full_config_json;
Ok ()
+
(* Verification. *)
-let check_availability config_solver =
+let check_availability config =
let module Filename = Caml.Filename in
- let solver_name = config_solver.name in
- Logs.info (fun m -> m "Checking actual availability of `%s'." solver_name);
+ Logs.debug
+ (fun m -> m "Checking actual availability of `%a'."
+ pp_solver config.solver);
try
(* 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]
+ config.exe
+ [default_option_of_solver config.solver]
in
+ Logs.debug
+ (fun m -> m "Executing command `%s' to check `%a' availability."
+ cmd
+ pp_solver config.solver);
let retcode = Sys.command cmd in
let in_channel = Stdlib.open_in tmp in
Stdlib.close_in in_channel;
@@ -276,14 +274,14 @@ let check_availability config_solver =
with Stdlib.Not_found | End_of_file | Failure _ | Sys_error _ ->
Error "Unexpected failure."
-let check_compatibility config_solver model =
- let solver = config_solver.solver in
+let check_compatibility config model =
+ let solver = config.solver in
match solver, model.Model.format with
| (Pyrat | Marabou), (Model.Onnx as f) ->
Error
- (Format.sprintf
- "No support yet for `%s' and model format `%s'."
- (show_solver solver)
+ (Format.asprintf
+ "No support yet for `%a' and model format `%s'."
+ pp_solver solver
(Model.show_format f))
| _ ->
Ok ()
@@ -341,19 +339,19 @@ let build_command ?raw_options confg_solver property model =
with Failure e ->
Error (Format.sprintf "Unexpected failure@ `%s'." e)
-let exec ?raw_options config_solver model property =
+let exec ?raw_options config model property =
let open Result in
(* Check solver availability. *)
- check_availability config_solver >>= fun () ->
+ check_availability config >>= fun () ->
(* Check solver and model compatibility. *)
- check_compatibility config_solver model >>= fun () ->
+ check_compatibility config model >>= fun () ->
(* Build the required command-line. *)
- build_command ?raw_options config_solver property model >>= fun (tmp, cmd) ->
+ build_command ?raw_options config property model >>= fun (tmp, cmd) ->
(* Execute the command. *)
begin
try
Logs.app
- (fun m -> m "Launching verification with `%s'." config_solver.name);
+ (fun m -> m "Launching verification with `%a'." pp_solver config.solver);
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 cb85fc70aad008b77af113f7e320e2ba111cd157..cc4aaae405d51f29f7d30e36e161cecaa241af22 100644
--- a/solver.mli
+++ b/solver.mli
@@ -10,25 +10,22 @@ 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_file: string
-val default_config_filename: string
-
-(** [detect file] searches for solvers in $PATH, or in the paths provided
- via [env_vars], and save the configurations in [file]. *)
-val detect: string -> (unit, string) Result.t
+(** [detect ~file] searches for solvers in $PATH, or in the path provided in env
+ variable $DIR, and save the configurations in [file]. *)
+val detect: file:string -> (unit, string) Result.t
(** Solver configuration. *)
-type config_solver
+type config
-(** [config_solver ~solver file] retrieves the [solver] configuration, if any,
- from the given [file]. *)
-val get_config_solver:
- solver:string -> string -> (config_solver, string) Result.t
+(** [get_config ~file solver] retrieves the [solver] configuration, if any, from
+ the given [file]. *)
+val get_config: file:string -> solver -> (config, string) Result.t
-(** [exec ?raw_options config_solver model property] runs [solver] wrt the given
- [config_solver] on [property] for [model] with the provided [raw_options], if
- any. *)
+(** [exec ?raw_options config model property] runs a solver wrt the given
+ [config] on [property] for [model] with the provided [raw_options], if any.
+*)
val exec:
?raw_options:string ->
- config_solver -> Model.t -> Property.t -> (unit, string) Result.t
+ config -> Model.t -> Property.t -> (unit, string) Result.t