From 1525ffdde00bc696f0e5de2d50adf9b8d0fa3ad1 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 14 Apr 2021 15:51:57 +0200
Subject: [PATCH] Rework property language and restructure code.
---
config.ml | 216 ++++++++++++
config.mli | 28 ++
dune | 7 +-
engine.ml | 259 +++++++++++++++
engine.mli | 11 +
main.ml | 28 +-
marabou.ml | 114 +++++++
property_syntax.mli => marabou.mli | 15 +-
model.ml | 1 +
property.ml | 249 ++++++++++----
property.mli | 40 ++-
property_lexer.mll | 66 ++--
property_parser.mly | 132 +++++---
property_types.mli | 35 ++
pyrat.ml | 55 ++++
pyrat.mli | 7 +
solver.ml | 508 ++---------------------------
solver.mli | 70 ++--
18 files changed, 1185 insertions(+), 656 deletions(-)
create mode 100644 config.ml
create mode 100644 config.mli
create mode 100644 engine.ml
create mode 100644 engine.mli
create mode 100644 marabou.ml
rename property_syntax.mli => marabou.mli (62%)
create mode 100644 property_types.mli
create mode 100644 pyrat.ml
create mode 100644 pyrat.mli
diff --git a/config.ml b/config.ml
new file mode 100644
index 0000000..cad1681
--- /dev/null
+++ b/config.ml
@@ -0,0 +1,216 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
+open Base
+
+module Format = Caml.Format
+module Sys = Caml.Sys
+module Filename = Caml.Filename
+
+type version =
+ | Unknown
+ | Version of string
+[@@deriving show { with_path = false }, yojson]
+
+type t = {
+ name: string;
+ exe: string;
+ version: version;
+}
+[@@deriving yojson, show]
+
+type full_config = t list [@@deriving yojson, show]
+
+let exe_path_of_solver solver =
+ let module S = (val solver: Solver.S) in
+ (* We want the complete path of [exe] in $PATH: we use `command -v [exe]'
+ and retrieve the result, if any. *)
+ let tmp = Filename.temp_file "caisar" "command" in
+ let _retcode =
+ Sys.command
+ (Filename.quote_command
+ ~stdout:tmp ~stderr:tmp
+ "command" ["-v"; S.exe_name])
+ in
+ let in_channel = Stdlib.open_in tmp in
+ let found, exe =
+ try true, Stdlib.input_line in_channel
+ with End_of_file -> false, S.exe_name
+ in
+ Stdlib.close_in in_channel;
+ Sys.remove tmp;
+ if found
+ then Ok exe
+ else begin
+ match Sys.getenv_opt "DIR" with
+ | None ->
+ Error (Format.asprintf "Cannot find the executable of `%s'." S.name)
+ | Some dir ->
+ (* The env variable should already provide the path to the executable: we
+ first check that the path exists, refers to a directory and it is
+ absolute, then we concatenate the [exe] name to it. *)
+ if not (Sys.file_exists dir && Sys.is_directory dir)
+ then
+ Error (Format.sprintf "`%s' not exist or is not a directory." dir)
+ else
+ if Filename.is_relative dir
+ then
+ Error
+ (Format.sprintf
+ "`%s' is a relative path. An absolute path is required for DIR."
+ dir)
+ else
+ let exe =
+ if Filename.check_suffix dir Filename.dir_sep
+ then dir ^ exe
+ else Format.sprintf "%s%s%s" dir Filename.dir_sep exe
+ in
+ Ok exe
+ end
+
+let version_of_solver solver s =
+ let module S = (val solver: Solver.S) in
+ try
+ (* We suppose that the first occurrence that matches [re_version] is indeed
+ the version of the concercend [solver]. *)
+ ignore (Str.search_forward S.re_version s 0);
+ Version (Str.matched_string s)
+ with Stdlib.Not_found ->
+ Logs.debug (fun m -> m "No recognizable version found.");
+ Unknown
+
+let default_config_file =
+ let filename = ".caisar.conf" in
+ match Sys.getenv_opt "HOME" with
+ | None -> filename
+ | Some p -> p ^ "/.caisar.conf"
+
+let retrieve_full_config file =
+ let open Result in
+ match full_config_of_yojson (Yojson.Safe.from_file file) with
+ | Error _ | exception _ ->
+ []
+ | Ok full_config ->
+ begin
+ Logs.debug (fun m ->
+ m "Configuration in file `%s':@ %a"
+ file
+ pp_full_config full_config);
+ full_config
+ end
+
+let retrieve ~file solver =
+ let open Result in
+ let module S = (val solver: Solver.S) in
+ Logs.info (fun m ->
+ m "Reading configuration file `%s' for solver `%s'." file S.name);
+ 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. *)
+ let full_config = retrieve_full_config file in
+ (* Search for a [config] with [solver]. *)
+ match List.find ~f:(fun cs -> String.equal cs.name S.name) full_config with
+ | None ->
+ Error
+ (Format.asprintf
+ "No solver `%s' found in configuration file `%s'."
+ S.name file)
+ | Some ({ name; version; _ } as config) ->
+ begin
+ Logs.info (fun m -> m "Found `%s' `%s'." name (show_version version));
+ Ok config
+ end
+ end
+
+(* All solver instances. *)
+let default_solvers =
+ [ (module Pyrat: Solver.S); (module Marabou: Solver.S) ]
+
+let detect_default_solvers () =
+ try
+ let config =
+ List.filter_map
+ ~f:(fun solver ->
+ match exe_path_of_solver solver with
+ | Error msg ->
+ Logs.info (fun m -> m "%s" msg);
+ None
+ | Ok exe ->
+ (* We detect whether solver is available in $PATH, or in the
+ provided path via env variable, by executing `solver
+ --version' command. *)
+ let module S = (val solver: Solver.S) in
+ let tmp = Filename.temp_file "caisar" "detect" in
+ let cmd =
+ Filename.quote_command
+ ~stdout:tmp ~stderr:tmp
+ exe
+ [S.exe_default_option]
+ in
+ Logs.debug (fun m ->
+ m "Executing command `%s' to detect `%s'."
+ cmd S.name);
+ let retcode = Sys.command cmd in
+ let cmd_output =
+ let in_channel = Stdlib.open_in tmp in
+ let buf = Buffer.create 512 in
+ try
+ while true do
+ Stdlib.Buffer.add_channel buf in_channel 512;
+ done;
+ assert false
+ with End_of_file ->
+ Stdlib.close_in in_channel;
+ Buffer.contents buf
+ in
+ Sys.remove tmp;
+ if retcode <> 0
+ then begin
+ Logs.info (fun m -> m "No solver `%s' found." S.name);
+ None
+ end
+ else begin
+ (* If available, we save a [config] for solver. *)
+ let version = version_of_solver solver cmd_output in
+ let config = { name = S.name; exe; version; } in
+ Logs.app (fun m ->
+ m "Found solver `%s' `%a' (%s)."
+ S.name
+ pp_version version
+ exe);
+ Some config
+ end)
+ default_solvers
+ in
+ Ok config
+ with _ ->
+ Error "Unexpected failure."
+
+let detect ~file =
+ let open Result in
+ (* Detect default supported solvers in $PATH or $DIR. *)
+ detect_default_solvers () >>= fun default_full_config ->
+ (* Retrieve the current configuration from [file]. *)
+ let current_full_config = retrieve_full_config file in
+ (* Create new configuration file. *)
+ Logs.debug (fun m -> m "Creating new configuration file `%s'." file);
+ let out_channel = Stdlib.open_out file in
+ (* 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 = String.compare cs1.name cs2.name 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 full_config_json = full_config_to_yojson full_config in
+ Yojson.Safe.pretty_to_channel out_channel full_config_json;
+ Stdlib.close_out out_channel;
+ Ok ()
diff --git a/config.mli b/config.mli
new file mode 100644
index 0000000..cfb1caa
--- /dev/null
+++ b/config.mli
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
+type version =
+ | Unknown
+ | Version of string
+
+type t = private {
+ name: string;
+ exe: string;
+ version: version;
+}
+
+(** Path to default configuration file. *)
+val default_config_file: string
+
+(** The list of supported solvers by default. *)
+val default_solvers: Solver.instance list
+
+(** [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
+
+(** @return the [solver] configuration, if any, from the given [file]. *)
+val retrieve: file:string -> Solver.instance -> (t, string) Result.t
diff --git a/dune b/dune
index 2bc8efe..4ec3915 100644
--- a/dune
+++ b/dune
@@ -2,11 +2,12 @@
(modules property_lexer))
(menhir
- (modules property_parser))
+ (modules property_parser)
+ (flags --table))
(executable
(name main)
(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)
+ (modules_without_implementation property_types)
+ (libraries menhirLib 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 ppx_deriving.eq)))
diff --git a/engine.ml b/engine.ml
new file mode 100644
index 0000000..c66f486
--- /dev/null
+++ b/engine.ml
@@ -0,0 +1,259 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
+open Base
+open Property_types
+
+module Format = Caml.Format
+module Sys = Caml.Sys
+module Filename = Caml.Filename
+
+(* Verification task submitted to a solver. *)
+type task = {
+ (* Identifier. *)
+ id: string;
+ (* Original goal name. *)
+ goalname: string;
+ (* Subgoal identifier.
+ Typically a goal is translated to multiple subgoals by a solver. *)
+ subgoal: int;
+ (* The formula to verify. *)
+ formula: string;
+ (* Verification result.
+ [None] means no verification yet. *)
+ result: (Solver.Result.t, string) Result.t option;
+}
+
+let check_availability solver config =
+ let module S = (val solver: Solver.S) in
+ Logs.debug (fun m -> m "Checking actual availability of `%s'." S.name);
+ 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.Config.exe
+ [S.exe_default_option]
+ in
+ Logs.debug (fun m ->
+ m "Executing command `%s' to check `%s' availability." cmd S.name);
+ 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. \
+ 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 module S = (val solver: Solver.S) in
+ if S.is_model_format_supported model.Model.format
+ then Ok ()
+ else
+ Error
+ (Format.asprintf
+ "No support yet for `%s' and model format `%s'."
+ S.name
+ (Model.show_format model.format))
+
+let tasks_of_property solver { hypothesis; goals } =
+ let module S = (val solver: Solver.S) in
+ let table = Hashtbl.create (module String) in
+ List.iter
+ goals
+ ~f:(fun { name; formula; } ->
+ let elts = S.(repr (translate ~hypothesis ~goal:formula)) in
+ let tasks =
+ List.mapi
+ elts
+ ~f:(fun idx elt ->
+ { id = Format.sprintf "%s.%d" name idx;
+ goalname = name;
+ subgoal = idx;
+ formula = Format.asprintf "%a" S.pretty elt;
+ result = None; })
+ in
+ Hashtbl.set table ~key:name ~data:tasks);
+ table
+
+let build_command ~raw_options solver config model task =
+ let open Result in
+ let module S = (val solver: Solver.S) in
+ (* Write property to temporary file. *)
+ begin
+ try
+ let tmp = Filename.temp_file "prop" S.name in
+ let out_channel = Stdlib.open_out tmp in
+ let fmt = Format.formatter_of_out_channel out_channel in
+ Format.fprintf fmt "%s@?" task.formula;
+ Stdlib.close_out out_channel;
+ Ok tmp
+ with Sys_error e ->
+ Error (Format.sprintf "Unexpected failure:@ %s." e)
+ end >>= fun property ->
+ (* Build actual command-line. *)
+ try
+ let log = Filename.temp_file "log" S.name in
+ let output = Filename.temp_file "output" S.name in
+ let options = S.options ~model:model.Model.filename ~property ~output in
+ let command =
+ let args = options @ raw_options in
+ Filename.quote_command ~stdout:log ~stderr:log config.Config.exe args
+ in
+ Ok (command, property, log, output)
+ with Failure e ->
+ Error (Format.sprintf "Unexpected failure:@ %s." e)
+
+let extract_result solver ~log ~output =
+ let module S = (val solver: Solver.S) in
+ Logs.info (fun m -> m "Extracting result of verification.");
+ let output =
+ let content file =
+ let in_channel = Stdlib.open_in file in
+ let buf = Buffer.create 512 in
+ try
+ while true do
+ Stdlib.Buffer.add_channel buf in_channel 512;
+ done;
+ assert false
+ with End_of_file ->
+ Stdlib.close_in in_channel;
+ buf
+ in
+ let output = content output in
+ if Buffer.length output > 0
+ then output
+ else content log
+ in
+ let output = Buffer.contents output in
+ let results = [ Solver.Result.Valid; Invalid; Timeout; Unknown ] in
+ List.fold
+ results
+ ~init:Solver.Result.Failure
+ ~f:(fun acc result ->
+ let regexp = S.re_of_result result in
+ let found =
+ try Str.search_forward regexp output 0 >= 0
+ with Stdlib.Not_found -> false
+ in
+ if found
+ then result
+ else acc)
+
+let exec_tasks ~raw_options solver config model tasks_htbl =
+ let module S = (val solver: Solver.S) in
+ let open Result in
+ Logs.app (fun m -> m "Launching verification with `%s'." S.name);
+ (* Run one task at a time and modify its status. *)
+ Hashtbl.map_inplace
+ tasks_htbl
+ ~f:(fun tasks ->
+ List.map
+ tasks
+ ~f:(fun task ->
+ Logs.app (fun m ->
+ m "Verifying goal `%s', subgoal %d (%s)."
+ task.goalname task.subgoal task.id);
+ let res_exec_task =
+ (* Build the required command-line. *)
+ build_command ~raw_options solver config model task
+ >>= fun (cmd, prop, log, output) ->
+ (* Execute the command. *)
+ Logs.info (fun m -> m "Executing command `%s'." cmd);
+ try
+ let retcode = Sys.command cmd in
+ Sys.remove prop;
+ if retcode <> 0
+ then Error (Format.sprintf "Command `%s' has failed." cmd)
+ else begin
+ (* Extract and pretty-print verification result. *)
+ let result = extract_result solver ~log ~output in
+ Logs.app (fun m -> m "Result %s: %a."
+ task.id Solver.Result.pretty result);
+ Sys.remove output;
+ if Solver.Result.equal result Solver.Result.Failure
+ then
+ Logs.app (fun m ->
+ m "See error messages in `%s' for more information."
+ log)
+ else
+ Sys.remove log;
+ Ok result
+ end
+ with _ ->
+ Error "Unexpected failure."
+ in
+ { task with result = Some res_exec_task; }));
+ tasks_htbl
+
+let consolidate_task_results solver tasks_htbl =
+ let module S = (val solver: Solver.S) in
+ Hashtbl.map
+ tasks_htbl
+ ~f:(fun tasks ->
+ let consolidated_result =
+ List.fold tasks ~init:None
+ ~f:(fun accum { result; _ } ->
+ let result =
+ match result with
+ | None -> None
+ | Some Ok result -> Some result
+ | Some Error _ -> Some Failure
+ in
+ match accum, result with
+ | _, None -> accum
+ | None, result -> result
+ | Some r1, Some r2 -> Some (S.consolidate r1 r2))
+ in
+ consolidated_result, tasks)
+
+let pretty_summary tasks_htbl =
+ let pretty_task_status fmt { id; result; _ } =
+ let result = Option.value_exn result in
+ let result_string =
+ match result with
+ | Ok r -> Format.asprintf "%a" Solver.Result.pretty r
+ | Error msg -> msg
+ in
+ Format.fprintf fmt "@[-- %s: @[<hov>%s@]@]" id result_string
+ in
+ let pretty_goal_tasks fmt (goalname, (consolidated_result, tasks)) =
+ Format.fprintf fmt "@[- %s: @[<v>%a@ %a@]@]"
+ goalname
+ Solver.Result.pretty (Option.value_exn consolidated_result)
+ (Format.pp_print_list ~pp_sep:Format.pp_print_space pretty_task_status)
+ tasks
+ in
+ Logs.app (fun m ->
+ m "@[<v 2>Summary:@ %a@]"
+ (Format.pp_print_list ~pp_sep:Format.pp_print_space pretty_goal_tasks)
+ (Hashtbl.to_alist tasks_htbl))
+
+let exec ~raw_options solver config model property =
+ let open Result in
+ let module S = (val solver: Solver.S) in
+ (* Check solver availability. *)
+ check_availability solver config >>= fun () ->
+ (* Check solver and model compatibility. *)
+ check_compatibility solver model >>= fun () ->
+ (* Translate property into tasks. *)
+ tasks_of_property solver property |>
+ (* Run verification process. *)
+ exec_tasks ~raw_options solver config model |>
+ (* Consolidate task results for every goal. *)
+ consolidate_task_results solver |>
+ (* Pretty print a summary on results. *)
+ pretty_summary |> fun () ->
+ Ok ()
diff --git a/engine.mli b/engine.mli
new file mode 100644
index 0000000..ad36710
--- /dev/null
+++ b/engine.mli
@@ -0,0 +1,11 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
+(** [exec ~raw_options config model property] runs a solver wrt the given
+ [config] on [property] for [model] with the provided [raw_options]. *)
+val exec:
+ raw_options:string list ->
+ Solver.instance -> Config.t -> Model.t -> Property.t -> (unit, string) Result.t
diff --git a/main.ml b/main.ml
index 6cdafd5..425cc9d 100644
--- a/main.ml
+++ b/main.ml
@@ -6,6 +6,7 @@
open Base
open Cmdliner
+
module Format = Caml.Format
let caisar = "caisar"
@@ -50,23 +51,24 @@ let config cmd detect file () =
(fun m -> m "Command `%s' with configuration file `%s'." cmd file);
if detect
then begin
- match Solver.detect ~file with
+ match Config.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_file model property solver () =
+ let module S = (val solver: Solver.S) in
Logs.debug
(fun m ->
m "Command `%s' with@ model `%s',@ property `%s' and@ solver `%s' \
(using configuration file `%s')."
- cmd model property (Solver.show_solver solver) config_file);
+ cmd model property S.name 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 ~file:config_file >>= fun config ->
- Solver.exec ~raw_options config model property
+ Config.retrieve ~file:config_file solver >>= fun config ->
+ Engine.exec ~raw_options solver config model property
in
match do_verify () with
| Ok () -> Logs.app (fun m -> m "Done.")
@@ -95,7 +97,7 @@ let config_cmd =
let doc =
Format.sprintf "$(b,FILE) to write the %s configuration to." caisar
in
- Arg.(value & pos 0 string Solver.default_config_file
+ Arg.(value & pos 0 string Config.default_config_file
& info [] ~docv:docv_filename ~doc)
in
let doc = Format.sprintf "%s configuration." caisar in
@@ -120,7 +122,11 @@ let verify_cmd =
let docv_solver = "SOLVER" in
let solver =
let solver_names =
- List.map ~f:(fun s -> String.lowercase (Solver.show s)) Solver.defaults
+ List.map
+ Config.default_solvers
+ ~f:(fun solver ->
+ let module S = (val solver: Solver.S) in
+ String.lowercase S.name)
in
let doc =
Format.asprintf
@@ -134,11 +140,13 @@ let verify_cmd =
let solvers =
Arg.enum
(List.map
- ~f:(fun s -> String.lowercase (Solver.show_solver s), s)
- Solver.defaults)
+ Config.default_solvers
+ ~f:(fun solver ->
+ let module S = (val solver: Solver.S) in
+ String.lowercase S.name, solver))
in
Arg.(required
- & pos 2 (some solvers) (Some Solver.Pyrat)
+ & pos 2 (some solvers) (Some (module Pyrat: Solver.S))
& info [] ~docv:docv_solver ~doc)
in
let docv_model = "MODEL" in
@@ -158,7 +166,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_file
+ Arg.(value & opt file Config.default_config_file
& info ["c"; "config"] ~doc)
in
let doc = "Property verification of neural networks." in
diff --git a/marabou.ml b/marabou.ml
new file mode 100644
index 0000000..1fbe98f
--- /dev/null
+++ b/marabou.ml
@@ -0,0 +1,114 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
+open Property_types
+
+type t = Property.disjunct Property.nform
+
+let name = "Marabou"
+let exe_name = "Marabou"
+let exe_default_option = "--version"
+let re_version = Str.regexp "[0-9]\\(\\.[0-9]\\)*\\(\\.?[A-Za-z-+]\\)*"
+
+let re_of_result result =
+ Str.regexp
+ (match result with
+ | Solver.Result.Valid -> "\\(s\\|S\\)at\\|SAT"
+ | Invalid -> "\\(u\\|U\\)nsat\\|UNSAT"
+ | Timeout -> "\\(t\\|T\\)imeout\\|TIMEOUT"
+ | Unknown -> "\\(u\\|U\\)nknown\\|UNKNOWN"
+ | Failure -> assert false)
+
+let is_model_format_supported = function
+ | Model.Nnet _ -> true
+ | Onnx -> false
+
+let options ~model ~property ~output =
+ let verbosity_level =
+ match Logs.level () with
+ | None | Some (App | Error | Warning) -> 0
+ | Some Info -> 1
+ | Some Debug -> 2
+ in
+ [ "--property"; property;
+ "--input"; model;
+ "--verbosity"; Int.to_string verbosity_level;
+ "--summary-file"; output ]
+
+let consolidate r1 r2=
+ match r1, r2 with
+ | _, Solver.Result.Valid | Solver.Result.Valid, _ -> Solver.Result.Valid
+ | Invalid, result | result, Invalid -> result
+ | Failure, _ | _, Failure -> Failure
+ | Timeout, _ | _, Timeout -> Timeout
+ | Unknown, Unknown -> Unknown
+
+(* Transform [k_y_0 + ky_1 + ... + ky_n cop ky_n+1] into [ky_n+1 + k_y_0 +
+ ky_1 + ... + ky_n cop 0], taking care of the sign. *)
+let rec constant_rhs formula =
+ match formula with
+ | Constraint (terms, cop, General (sign_opt, cst_opt, var)) ->
+ let terms =
+ match sign_opt, cst_opt with
+ | _, Some Int i when i = 0 -> terms
+ | _, Some Float f when Base.Float.(=) f 0. -> terms
+ | (None | Some Plus), None ->
+ General (Some Minus, None, var) :: terms
+ | (None | Some Plus), Some cst ->
+ let negcst =
+ match cst with
+ | Int i -> Int (~- i)
+ | Float f -> Float (~-. f)
+ in
+ General (Some Plus, Some negcst, var) :: terms
+ | Some Minus, _ ->
+ General (Some Plus, cst_opt, var) :: terms
+ in
+ Constraint (terms, cop, Constant (Int 0))
+ | Constraint (_, _, Constant _) ->
+ formula
+ | And (p1, p2) ->
+ And (constant_rhs p1, constant_rhs p2)
+ | Or (p1, p2) ->
+ Or (constant_rhs p1, constant_rhs p2)
+
+let translate ~hypothesis ~goal =
+ let goal = constant_rhs goal in
+ Property.dnf_of_formula (And (hypothesis, goal))
+
+let repr = Property.get_disjuncts
+
+let pretty fmt t =
+ let pp_terms fmt terms =
+ match terms with
+ | [] ->
+ assert false (* Terms are non-empty lists by construction. *)
+ | [ t ] ->
+ Property.pretty_term fmt t
+ | t :: tt ->
+ let pp_term = Property.pretty_term ~pp_sign:true in
+ Format.fprintf fmt "@[%a %a@]"
+ pp_term t
+ (Format.pp_print_list
+ ~pp_sep:(fun fmt () -> Format.pp_print_char fmt ' ')
+ pp_term) tt
+ in
+ let rec pp_formula fmt formula =
+ match formula with
+ | Constraint (terms, cop, term) ->
+ Format.fprintf fmt "%a %a %a"
+ pp_terms terms
+ Property.pretty_cop cop
+ (Property.pretty_term ~pp_sign:true) term
+ | And (p1, p2) ->
+ Format.fprintf fmt "%a@\n%a" pp_formula p1 pp_formula p2
+ | Or _ ->
+ (* Marabou does not handle Or connectives directly. Anyway, it should
+ not happen as in [translate] we convert the original goal into a
+ dnf-like form where we retrieve only the final conjuncts. *)
+ assert false
+ in
+ Format.fprintf fmt "@[%a@]" pp_formula t
diff --git a/property_syntax.mli b/marabou.mli
similarity index 62%
rename from property_syntax.mli
rename to marabou.mli
index c81a3ea..8cf7a73 100644
--- a/property_syntax.mli
+++ b/marabou.mli
@@ -4,17 +4,4 @@
(* *)
(**************************************************************************)
-type var =
- | Input of string
- | Output of string
-
-type cop = Eq | Ge | Le | Gt | Lt
-
-type cst =
- | Int of int
- | Float of float
-
-type t =
- | Atomic_cst of var * cop * cst
- | Atomic_var of var * cop * var
- | And of t * t
+include Solver.S
diff --git a/model.ml b/model.ml
index a9d8bdc..528ec20 100644
--- a/model.ml
+++ b/model.ml
@@ -5,6 +5,7 @@
(**************************************************************************)
open Base
+
module Format = Caml.Format
module Sys = Caml.Sys
module Filename = Caml.Filename
diff --git a/property.ml b/property.ml
index f677587..c749d47 100644
--- a/property.ml
+++ b/property.ml
@@ -5,66 +5,64 @@
(**************************************************************************)
open Base
+open Property_types
+
module Format = Caml.Format
module Sys = Caml.Sys
+module Lexer = Property_lexer
+module Parser = Property_parser
+module MI = Parser.MenhirInterpreter
+module ER = MenhirLib.ErrorReports
+module LU = MenhirLib.LexerUtil
-type t = Property_syntax.t
-
-let do_build ~property line =
- let linebuf = Lexing.from_string line in
- try
- let p = Property_parser.main Property_lexer.token linebuf in
- let property =
- Option.value_map
- property
- ~default:p
- ~f:(fun p' -> Property_syntax.And (p', p))
- in
- Ok property
+type t = Property_types.t
+type 'a printer = Caml.Format.formatter -> 'a -> unit
+
+(* [show text (pos1, pos2)] displays a range of the input text [text]
+ delimited by the positions [pos1] and [pos2]. *)
+let show text positions =
+ ER.extract text positions
+ |> ER.sanitize
+ |> ER.compress
+ |> ER.shorten 20 (* max width 43 *)
+
+(* The parser has succeeded and produced a property. *)
+let succeed (property: t) =
+ Ok property
+
+(* The parser has encountered a syntax error. *)
+let fail text buffer (_ : t MI.checkpoint) =
+ (* Indicate where in the input file the error occurred. *)
+ let location = LU.range (ER.last buffer) in
+ (* Show the tokens just before and just after the error. *)
+ let indication =
+ Format.sprintf "Syntax error %s." (ER.show (show text) buffer)
+ in
+ (* Show these three components. *)
+ Error (Format.sprintf "%s%s" location indication)
+
+let build ~filename =
+ (* Read the file; allocate and initialize a lexing buffer. *)
+ let text, lexbuf = LU.read filename in
+ (* Wrap the lexer and lexbuf together into a supplier, that is, a
+ function of type [unit -> token * position * position]. *)
+ let supplier = MI.lexer_lexbuf_to_supplier Lexer.token lexbuf in
+ (* Equip the supplier with a two-place buffer that records the positions
+ of the last two tokens. This is useful when a syntax error occurs, as
+ these are the token just before and just after the error. *)
+ let buffer, supplier = ER.wrap_supplier supplier in
+ (* Fetch the parser's initial checkpoint. *)
+ let checkpoint = Parser.Incremental.main lexbuf.lex_curr_p in
+ (* Run the parser. *)
+ try MI.loop_handle succeed (fail text buffer) supplier checkpoint
with
| Property_lexer.Error msg ->
Error (Format.sprintf "%s" msg)
- | Property_parser.Error ->
- Error
- (Format.sprintf
- "Property syntax error at offset %d."
- (Lexing.lexeme_start linebuf))
-let build ~filename =
- if Sys.file_exists filename
- then
- let in_channel = Stdlib.open_in filename in
- let rec read_one_line ~property channel =
- let line_opt, continue = Property_lexer.line channel in
- if not continue
- then begin
- Stdlib.close_in in_channel;
- Result.of_option
- property
- ~error:(Format.sprintf "No property found in `%s'." filename)
- end
- else begin
- let property_or_error =
- (* Since [continue] is true, there is a line by lexer construction. *)
- let line = Option.value_exn line_opt in
- do_build ~property line
- in
- Result.join
- (Result.map
- property_or_error
- ~f:(fun p -> read_one_line ~property:(Some p) channel))
- end
- in
- read_one_line ~property:None (Lexing.from_channel in_channel)
- else
- Error (Format.sprintf "No such file `%s'." filename)
-
-let rec repr t =
- let open Property_syntax in
- let string_of_var = function
- | Input s -> Format.sprintf "Input %s" s
- | Output s -> Format.sprintf "Output %s" s
- in
+
+(* Printing. *)
+
+let pretty_cop fmt cop =
let string_of_cop = function
| Eq -> "="
| Ge -> ">="
@@ -72,23 +70,134 @@ let rec repr t =
| Gt -> ">"
| Lt -> "<"
in
- let string_of_cst = function
- | Int i -> Format.sprintf "int %d" i
- | Float f -> Format.sprintf "float %f" f
- in
- match t with
- | Atomic_cst (var, cop, cst) ->
- let var_s = string_of_var var in
- let cop_s = string_of_cop cop in
- let cst_s = string_of_cst cst in
- Format.sprintf "%s %s %s" var_s cop_s cst_s
- | Atomic_var (var1, cop, var2) ->
- let var1_s = string_of_var var1 in
- let cop_s = string_of_cop cop in
- let var2_s = string_of_var var2 in
- Format.sprintf "%s %s %s" var1_s cop_s var2_s
+ Format.pp_print_string fmt (string_of_cop cop)
+
+let pretty_var fmt = function
+ | Input s | Output s -> Format.pp_print_string fmt s
+
+let pretty_cst fmt = function
+ | Int i -> Format.fprintf fmt "%d" i
+ | Float f -> Format.fprintf fmt "%f" f
+
+let pretty_term ?(pp_sign=false) fmt = function
+ | Constant cst ->
+ pretty_cst fmt cst
+ | General (sign_opt, cst_opt, var) ->
+ begin match sign_opt, cst_opt with
+ | _, Some Int i when i = 0 -> ()
+ | _, Some Float f when Float.(=) f 0. -> ()
+ | (None | Some Plus), None ->
+ Format.fprintf fmt "@[%s%a@]"
+ (if not pp_sign then "" else "+")
+ pretty_var var
+ | (None | Some Plus), Some cst ->
+ let is_cst_negative =
+ match cst with
+ | Int i -> Int.is_negative i
+ | Float f -> Float.is_negative f
+ in
+ Format.fprintf fmt "@[%s%a%a@]"
+ (if not pp_sign || is_cst_negative then "" else "+")
+ pretty_cst cst
+ pretty_var var
+ | Some Minus, None ->
+ Format.fprintf fmt "@[-%a@]" pretty_var var
+ | Some Minus, Some cst ->
+ let negcst, is_negcst_negative =
+ match cst with
+ | Int i -> Int (~- i), i > 0
+ | Float f -> Float (~-. f), Float.(>) f 0.
+ in
+ Format.fprintf fmt "@[%s%a%a@]"
+ (if not pp_sign || is_negcst_negative then "" else "+")
+ pretty_cst negcst
+ pretty_var var
+ end
+
+let pretty_terms pp_term fmt terms =
+ match terms with
+ | [] ->
+ assert false (* Terms are non-empty lists by construction. *)
+ | [ t ] ->
+ pp_term fmt t
+ | t :: tt ->
+ Format.fprintf fmt "@[%a %a@]"
+ pp_term t
+ (Format.pp_print_list
+ ~pp_sep:(fun fmt () -> Format.pp_print_char fmt ' ')
+ pp_term) tt
+
+let rec pretty_formula fmt formula =
+ match formula with
+ | Constraint ([], _, _) ->
+ (* Non-empty list by construction. *)
+ assert false
+ | Constraint (terms, cop, term) ->
+ Format.fprintf fmt "@[%a %a %a@]"
+ (pretty_terms pretty_term) terms
+ pretty_cop cop
+ (pretty_term ~pp_sign:false) term
| And (p1, p2) ->
- Format.sprintf "And (%s, %s)" (repr p1) (repr p2)
+ Format.fprintf fmt "@[%a@ &&@ %a@]" pretty_formula p1 pretty_formula p2
+ | Or (p1, p2) ->
+ Format.fprintf fmt "@[%a@ ||@ %a@]" pretty_formula p1 pretty_formula p2
+
+let pretty_goal fmt goal =
+ Format.fprintf fmt "@[<v 2>goal %s:@ @[<hov>%a@]@]"
+ goal.name
+ pretty_formula goal.formula
let pretty fmt t =
- ignore (fmt, t)
+ Format.fprintf fmt "@[%a@]@\n@[<v>%a@]"
+ pretty_formula t.hypothesis
+ (Format.pp_print_list pretty_goal) t.goals
+
+
+(* Normal forms. *)
+
+type conjunct = formula
+type disjunct = formula
+type 'a nform = formula list
+
+let combine ~f f1 f2 =
+ if List.is_empty f1 || List.is_empty f2
+ then assert false
+ else begin
+ let rec loop (l1: formula list) l2 acc =
+ match l1 with
+ | [] ->
+ acc
+ | t :: tt ->
+ loop tt l2 List.(rev_append (map ~f:(fun x -> f t x) l2) acc)
+ in
+ List.rev (loop f1 f2 [])
+ end
+
+let rec convert_to_nf ~and_ ~or_ formula =
+ match formula with
+ | Constraint _ ->
+ [ formula ]
+ | And (p1, p2) ->
+ and_ (convert_to_nf ~and_ ~or_ p1) (convert_to_nf ~and_ ~or_ p2)
+ | Or (p1, p2) ->
+ or_ (convert_to_nf ~and_ ~or_ p1) (convert_to_nf ~and_ ~or_ p2)
+
+let cnf_of_formula (formula: formula) =
+ let and_ = function
+ | [] -> assert false
+ | [ _ ] as f -> f
+ | t :: tt -> [ List.fold tt ~init:t ~f:(fun acc f -> And (acc, f)) ]
+ in
+ convert_to_nf
+ ~and_:(fun l1 l2 -> and_ (List.append l1 l2))
+ ~or_:(combine ~f:(fun x y -> Or (x, y)))
+ formula
+
+let dnf_of_formula (formula: formula) =
+ convert_to_nf
+ ~and_:(combine ~f:(fun x y -> And (x, y)))
+ ~or_:List.append
+ formula
+
+let get_conjuncts = Fn.id
+let get_disjuncts = Fn.id
diff --git a/property.mli b/property.mli
index 34a1ee6..56dc81f 100644
--- a/property.mli
+++ b/property.mli
@@ -5,15 +5,47 @@
(**************************************************************************)
open Base
+open Property_types
-(** A property. *)
-type t = Property_syntax.t
+type t = Property_types.t
(** Builds a property out of the content of the given [filename], if possible. *)
val build: filename:string -> (t, string) Result.t
-(** Provides the raw representation of the given property. *)
-val repr: t -> string
+(** {2 Pretty printing.} *)
+
+type 'a printer = Caml.Format.formatter -> 'a -> unit
+
+(** Comparison operator pretty printer. *)
+val pretty_cop: cop printer
+
+(** Variable pretty printer. *)
+val pretty_var: var printer
+
+(** Constant pretty printer. *)
+val pretty_cst: constant printer
+
+(** Term pretty printer.
+ @param pp_sign determines whether the printer should print the sign also
+ for monomial terms.
+*)
+val pretty_term: ?pp_sign:bool -> term printer
+
+(** Term list pretty printer given one for a term. *)
+val pretty_terms: term printer -> term list printer
(** [pretty property] pretty prints [property]. *)
val pretty: Caml.Format.formatter -> t -> unit
+
+
+(** {2 Normal forms.} *)
+
+type conjunct
+type disjunct
+type 'a nform
+
+val cnf_of_formula: formula -> conjunct nform
+val dnf_of_formula: formula -> disjunct nform
+
+val get_conjuncts: conjunct nform -> formula list
+val get_disjuncts: disjunct nform -> formula list
diff --git a/property_lexer.mll b/property_lexer.mll
index a08e5fb..e066004 100644
--- a/property_lexer.mll
+++ b/property_lexer.mll
@@ -11,35 +11,49 @@
let input = 'x'['0'-'9']+
let output = 'y'['0'-'9']+
-(* This rule looks for a single line, terminated with '\n' or eof. It returns a
- pair of an optional string, the line that was found, and a Boolean flag,
- false if eof was reached. *)
-
-rule line = parse
-| ([^'\n']* '\n') as line
- (* Normal case: one line, no eof. *)
- { Some line, true }
-| eof
- (* Normal case: no data, eof. *)
- { None, false }
-| ([^'\n']+ as line) eof
- (* Special case: some data but missing '\n', then eof.
- Consider this as the last line, and add the missing '\n'. *)
- { Some (line ^ "\n"), false }
+(* Keywords. *)
+
+let goal = "goal"
+
+(* Macros. *)
+
+let space = [' ' '\t' '\r']
+
+let dec = ['0'-'9']
+let dec_sep = ['0'-'9' '_']
+
+let lalpha = ['a'-'z']
+let ualpha = ['A'-'Z']
+let alpha = (lalpha | ualpha)
-(* This rule analyzes a single line and turns it into a stream of tokens. *)
+let suffix = (alpha | dec_sep)*
+let ident = alpha suffix
-and token = parse
+
+(* This rule analyzes multiple lines until eof and turns them into a stream of
+ tokens. *)
+
+rule token = parse
| [' ' '\t' '\r']
{ token lexbuf }
+| '\n'
+ { MenhirLib.LexerUtil.newline lexbuf; token lexbuf }
| input as i
{ INPUT i }
| output as o
{ OUTPUT o }
-| '-'?['0'-'9']+'.'['0'-'9']+ as f
+| goal
+ { GOAL }
+| (ident as gid) space* ":"
+ { GOALID gid }
+| ('-'|'+')?['0'-'9']+'.'['0'-'9']+ as f
{ FLOAT (float_of_string f) }
-| '-'?['0'-'9']+ as i
+| ('-'|'+')?['0'-'9']+ as i
{ INT (int_of_string i) }
+| "+"
+ { PLUS }
+| "-"
+ { MINUS }
| "="
{ EQ }
| ">"
@@ -50,7 +64,15 @@ and token = parse
{ GE }
| "<="
{ LE }
-| '\n'
- { EOL }
+| "&&"
+ { AND }
+| "||"
+ { OR }
+| '('
+ { LPAREN }
+| ')'
+ { RPAREN }
+| eof
+ { EOF }
| _
- { raise (Error (Printf.sprintf "Property lexer at offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) }
+ { raise (Error (Format.sprintf "Property lexer at offset %d: unexpected character." (Lexing.lexeme_start lexbuf))) }
diff --git a/property_parser.mly b/property_parser.mly
index 6cf5926..6bdb619 100644
--- a/property_parser.mly
+++ b/property_parser.mly
@@ -8,49 +8,103 @@
%token <int> INT
%token <float> FLOAT
-%token <string> INPUT OUTPUT
+%token <string> INPUT OUTPUT GOALID
%token EQ GT LT GE LE
-%token EOL
+%token PLUS MINUS
+%token AND OR
+%token LPAREN RPAREN
+%token GOAL
+%token EOF
(* Starting rule. *)
-%start <Property_syntax.t> main
-%{ open Property_syntax %}
+%start <Property_types.t> main
+%{ open Property_types %}
%%
-(* Rules. *)
-
-main:
-| p = property EOL
- { p }
-
-property:
-| var cop cst
- { Atomic_cst ($1, $2, $3) }
-| var cop var
- { Atomic_var ($1, $2, $3) }
-
-var:
-| i = INPUT
- { Input i }
-| o = OUTPUT
- { Output o }
-
-cst:
-| i = INT
- { Int i }
-| f = FLOAT
- { Float f }
-
-cop:
-| EQ
- { Eq }
-| GE
- { Ge }
-| LE
- { Le }
-| GT
- { Gt }
-| LT
- { Lt }
+(* -------------------------------------------------------------------------- *)
+
+(* We parse a property given by
+ a hypothesis
+ a non-empty list of goals
+ followed by an end-of-file. *)
+
+let main :=
+ ~ = hypothesis; goals = nonempty_list(goal); EOF; { { hypothesis; goals; } }
+
+(* A hypothesis is a conjunctive formula over constraints. *)
+
+let hypothesis ==
+ and_formula(constraint_)
+
+(* A goal has a name and a formula. *)
+
+let goal :=
+ GOAL; name = GOALID; ~ = formula; { { name; formula; } }
+
+(* A formula is given by disjunctions of conjuctions of (delimited) formulae. *)
+
+let formula ==
+ or_formula(and_formula(delimited_formula))
+
+(* A disjunctive formula is a left-associative list of formulae, separated by OR
+ (i.e. ||) connective. *)
+
+let or_formula(elem) :=
+ | elem
+ | ors = or_formula(elem); OR; ~ = elem; { Or (ors, elem) }
+
+(* A conjunctive formula is a left-associative list of formulae, separated by
+ AND (i.e. &&) connective. *)
+
+let and_formula(elem) :=
+ | elem
+ | ands = and_formula(elem); AND; ~ = elem; { And (ands, elem) }
+
+(* A delimited formula is
+ either a constraint
+ or a parenthesized formula. *)
+
+let delimited_formula :=
+ | constraint_
+ | delimited(LPAREN, formula, RPAREN)
+
+(* A constraint is the application of a comparison operator to a non-empty list
+ of terms and a constant or a term. *)
+
+let constraint_ :=
+ | terms = nonempty_list(term); ~ = cop; ~ = constant; { Constraint (terms, cop, Constant constant) }
+ | terms = nonempty_list(term); ~ = cop; ~ = term; { Constraint (terms, cop, term) }
+
+(* A term is a constant coupled with a variable, possibly with a sign. *)
+
+let term :=
+ s = ioption(sign); c = ioption(constant); ~ = variable; { General (s, c, variable) }
+
+(* A constant is an integer or float value. *)
+
+let constant :=
+ | ~ = INT; <Int>
+ | ~ = FLOAT; <Float>
+
+(* A variable is either input or output. *)
+
+let variable :=
+ | ~ = INPUT; <Input>
+ | ~ = OUTPUT; <Output>
+
+(* Signs. *)
+
+let sign ==
+ | PLUS; { Plus }
+ | MINUS; { Minus }
+
+(* Comparison operators. *)
+
+let cop ==
+ | EQ; { Eq }
+ | GE; { Ge }
+ | LE; { Le }
+ | GT; { Gt }
+ | LT; { Lt }
diff --git a/property_types.mli b/property_types.mli
new file mode 100644
index 0000000..dd315b2
--- /dev/null
+++ b/property_types.mli
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
+type cop = Eq | Ge | Le | Gt | Lt
+type sign = Plus | Minus
+
+type constant =
+ | Int of int
+ | Float of float
+
+type var =
+ | Input of string
+ | Output of string
+
+type term =
+ | Constant of constant
+ | General of sign option * constant option * var
+
+type formula =
+ | Constraint of term list * cop * term
+ | And of formula * formula
+ | Or of formula * formula
+
+type goal = {
+ name: string;
+ formula: formula;
+}
+
+type t = {
+ hypothesis: formula;
+ goals: goal list;
+}
diff --git a/pyrat.ml b/pyrat.ml
new file mode 100644
index 0000000..7ad8404
--- /dev/null
+++ b/pyrat.ml
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
+open Property_types
+
+type t = Property.conjunct Property.nform
+
+let name = "PyRAT"
+let exe_name = "pyrat.py"
+let exe_default_option = "-v"
+let re_version = Str.regexp "[0-9]\\(\\.[0-9]\\)*\\(\\.?[A-Za-z-+]\\)*"
+
+let re_of_result result =
+ Str.regexp
+ (match result with
+ | Solver.Result.Valid -> "True"
+ | Invalid -> "False"
+ | Timeout -> "Timeout"
+ | Unknown -> "Unknown"
+ | Failure -> assert false)
+
+let is_model_format_supported = function
+ | Model.Nnet _ -> true
+ | Onnx -> false
+
+let options ~model ~property ~output:_ =
+ model :: property ::
+ match Logs.level () with
+ | None | Some (App | Error | Warning) -> []
+ | Some (Info | Debug) -> [ "--verbose" ]
+
+let consolidate _r1 _r2 = assert false
+
+let translate ~hypothesis ~goal =
+ Property.cnf_of_formula (And (hypothesis, goal))
+
+let repr = Property.get_conjuncts
+
+let pretty fmt t =
+ let rec pp_formula fmt formula =
+ match formula with
+ | Constraint (terms, cop, term) ->
+ Format.fprintf fmt "%a %a %a"
+ Property.(pretty_terms (pretty_term ~pp_sign:false)) terms
+ Property.pretty_cop cop
+ (Property.pretty_term ~pp_sign:false) term
+ | And (p1, p2) ->
+ Format.fprintf fmt "%a@\n%a" pp_formula p1 pp_formula p2
+ | Or (p1, p2) ->
+ Format.fprintf fmt "%a or %a" pp_formula p1 pp_formula p2
+ in
+ Format.fprintf fmt "@[%a@]" pp_formula t
diff --git a/pyrat.mli b/pyrat.mli
new file mode 100644
index 0000000..8cf7a73
--- /dev/null
+++ b/pyrat.mli
@@ -0,0 +1,7 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
+include Solver.S
diff --git a/solver.ml b/solver.ml
index 858deba..6b7dc37 100644
--- a/solver.ml
+++ b/solver.ml
@@ -5,480 +5,38 @@
(**************************************************************************)
open Base
-module Format = Caml.Format
-module Sys = Caml.Sys
-module Filename = Caml.Filename
-
-(* Supported solvers. *)
-type solver =
- | Pyrat
- | Marabou
- [@@deriving show { with_path = false }, ord, eq, yojson]
-
-
-(* Utilities. *)
-
-let defaults = [ Pyrat; Marabou ]
-
-let rec pp_property_marabou property =
- let open Property_syntax in
- let string_of_cop = function
- | Eq -> "="
- | Ge -> ">="
- | Le -> "<="
- | Gt -> ">"
- | Lt -> "<"
- in
- let string_of_cst = function
- | Int i -> Stdlib.string_of_int i
- | Float f -> Stdlib.string_of_float f
- in
- match property with
- | Atomic_cst ((Input v | Output v), cop, cst) ->
- Format.sprintf "%s %s %s" v (string_of_cop cop) (string_of_cst cst)
- | Atomic_var ((Input v1 | Output v1), cop, (Input v2 | Output v2)) ->
- Format.sprintf "%s %s %s" v1 (string_of_cop cop) v2
- | And (p1, p2) ->
- let s1 = pp_property_marabou p1 in
- let s2 = pp_property_marabou p2 in
- Format.sprintf "%s\n%s" s1 s2
-
-let pp_property_pyrat = pp_property_marabou
-
-let pp_property solver property =
- match solver with
- | Pyrat ->
- Ok (pp_property_pyrat property)
- | Marabou ->
- Ok (pp_property_marabou property)
-
-let default_exe_name_of_solver = function
- | Pyrat -> "pyrat.py"
- | Marabou -> "Marabou"
-
-let default_option_of_solver = function
- | Pyrat -> "-v"
- | Marabou -> "--version"
-
-let exe_path_of_solver solver =
- let exe = default_exe_name_of_solver solver in
- (* We want the complete path of [exe] in $PATH: we use `command -v [exe]'
- and retrieve the result, if any. *)
- let tmp = Filename.temp_file "caisar" "command" in
- let _retcode =
- Sys.command
- (Filename.quote_command
- ~stdout:tmp ~stderr:tmp
- "command" ["-v"; exe])
- in
- let in_channel = Stdlib.open_in tmp in
- let found, exe =
- try true, Stdlib.input_line in_channel
- with End_of_file -> false, exe
- in
- Stdlib.close_in in_channel;
- Sys.remove tmp;
- if found
- then Ok exe
- else begin
- match Sys.getenv_opt "DIR" with
- | None ->
- Error
- (Format.asprintf "Cannot find the executable of `%a'." pp_solver solver)
- | Some dir ->
- (* The env variable should already provide the path to the executable: we
- first check that the path exists, refers to a directory and it is
- absolute, then we concatenate the [exe] name to it. *)
- if not (Sys.file_exists dir && Sys.is_directory dir)
- then
- Error (Format.sprintf "`%s' not exist or is not a directory." dir)
- else
- if Filename.is_relative dir
- then
- Error
- (Format.sprintf
- "`%s' is a relative path. An absolute path is required for DIR."
- dir)
- else
- let exe =
- if Filename.check_suffix dir Filename.dir_sep
- then dir ^ exe
- else Format.sprintf "%s%s%s" dir Filename.dir_sep exe
- in
- Ok exe
- end
-
-let string_valid_of_solver = function
- | Pyrat -> "True"
- | Marabou -> "\\(s\\|S\\)at\\|SAT"
-
-let string_invalid_of_solver = function
- | Pyrat -> "False"
- | Marabou -> "\\(u\\|U\\)nsat\\|UNSAT"
-
-let string_timeout_of_solver = function
- | Pyrat -> "Timeout"
- | Marabou -> "\\(t\\|T\\)imeout\\|TIMEOUT"
-
-let string_unknown_of_solver = function
- | Pyrat -> "Unknown"
- | Marabou -> "\\(u\\|U\\)nknown\\|UNKNOWN"
-
-
-(* Configuration. *)
-
-type version =
- | Unknown
- | Version of string
-[@@deriving show { with_path = false }, yojson]
+open Property_types
-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 =
- (* We use same pattern to extract solver version numbers for the moment. *)
- match solver with
- | Pyrat | Marabou ->
- (* We want to match for version string of the form '0.0.1alpha+'. *)
- "[0-9]\\(\\.[0-9]\\)*\\(\\.?[A-Za-z-+]\\)*"
- in
- let regexp_version = Str.regexp regexp_string in
- try
- (* We suppose that the first occurrence that matches [regexp_string] is
- indeed the version of the concercend [solver]. *)
- ignore (Str.search_forward regexp_version s 0);
- Version (Str.matched_string s)
- with Stdlib.Not_found ->
- Logs.debug (fun m -> m "No recognizable version found.");
- Unknown
-
-let default_config_file =
- let filename = ".caisar.conf" in
- match Sys.getenv_opt "HOME" with
- | None -> filename
- | Some p -> p ^ "/.caisar.conf"
-
-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 ~file solver =
- let open Result in
- Logs.info
- (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. *)
- 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.asprintf
- "No solver `%a' found in configuration file `%s'."
- pp_solver solver
- file)
- | Some config ->
- begin
- Logs.info
- (fun m -> m "Found `%a' `%s'."
- pp_solver config.solver
- (show_version config.version));
- Ok config
- end
- end
-
-let create_config_file file =
- Logs.debug (fun m -> m "Creating new configuration file `%s'." file);
- Stdlib.open_out file
-
-let detect_default_solvers () =
- try
- let config =
- List.filter_map
- ~f:(fun solver ->
- match exe_path_of_solver solver with
- | Error msg ->
- Logs.info (fun m -> m "%s" msg);
- None
- | Ok exe ->
- (* 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 cmd =
- Filename.quote_command
- ~stdout:tmp ~stderr:tmp
- 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 cmd_output =
- let in_channel = Stdlib.open_in tmp in
- let buf = Buffer.create 512 in
- try
- while true do
- Stdlib.Buffer.add_channel buf in_channel 512;
- done;
- assert false
- with End_of_file ->
- Stdlib.close_in in_channel;
- Buffer.contents buf
- in
- Sys.remove tmp;
- if retcode <> 0
- then begin
- Logs.info (fun m -> m "No solver `%a' found." pp_solver solver);
- None
- end
- else begin
- (* If available, we save a [config] for solver. *)
- let version = version_of_solver solver cmd_output in
- let config = { solver; exe; version; } in
- Logs.app
- (fun m -> m "Found solver `%a' `%a' (%s)."
- pp_solver solver
- pp_version version
- exe);
- Some config
- end)
- defaults
- in
- Ok config
- with _ ->
- Error "Unexpected failure."
-
-let detect ~file =
- let open Result in
- (* Detect default supported solvers in $PATH or $DIR. *)
- detect_default_solvers () >>= fun default_full_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
- (* 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 full_config_json = full_config_to_yojson full_config in
- Yojson.Safe.pretty_to_channel out_channel full_config_json;
- Stdlib.close_out out_channel;
- Ok ()
-
-
-(* Verification. *)
-
-(* Verification result. *)
-type result =
- | Valid
- | Invalid
- | Timeout
- | Unknown
- | Failure
-[@@deriving show { with_path = false }, eq]
-
-let check_availability config =
- 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.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;
- Sys.remove tmp;
- if retcode = 0
- then
- Ok ()
- else
- Error
- (Format.sprintf
- "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 config model =
- let solver = config.solver in
- match solver, model.Model.format with
- | (Pyrat | Marabou), (Model.Onnx as f) ->
- Error
- (Format.asprintf
- "No support yet for `%a' and model format `%s'."
- pp_solver solver
- (Model.show_format f))
- | _ ->
- Ok ()
-
-let build_command ~raw_options confg_solver property model =
- 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. *)
- begin
- try
- let tmp = Filename.temp_file "prop" (show_solver solver) in
- let out_channel = Stdlib.open_out tmp in
- let fmt = Format.formatter_of_out_channel out_channel in
- Format.fprintf fmt "%s@?" s;
- Stdlib.close_out out_channel;
- Ok tmp
- with Sys_error e ->
- Error (Format.sprintf "Unexpected failure:@ %s." e)
- end >>= fun prop ->
- (* Build actual command-line. *)
- try
- let stdout = Filename.temp_file "output" (show_solver solver) in
- let summary =
- match solver with
- | Pyrat -> None
- | Marabou -> Some (Filename.temp_file "summary" (show_solver solver))
- in
- let cmd =
- let exe = confg_solver.exe in
- let args =
- match solver with
- | Pyrat ->
- let verbose =
- match Logs.level () with
- | None | Some (App | Error | Warning) -> false
- | Some (Info | Debug) -> true
- in
- 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
- "--property" :: prop ::
- "--input" :: model.Model.filename ::
- "--verbosity" :: Int.to_string verbosity_level ::
- "--summary-file" :: Option.value_exn summary ::
- raw_options
- in
- Filename.quote_command ~stdout ~stderr:stdout exe args
- in
- Ok (prop, cmd, (stdout, summary))
- with Failure e ->
- Error (Format.sprintf "Unexpected failure:@ %s." e)
-
-let extract_result config stdout summary =
- Logs.info (fun m -> m "Extracting result of verification.");
- let solver = config.solver in
- let output =
- let file =
- match solver with
- | Pyrat -> stdout
- | Marabou -> Option.value_exn summary
- in
- let in_channel = Stdlib.open_in file in
- let buf = Buffer.create 512 in
- try
- while true do
- Stdlib.Buffer.add_channel buf in_channel 512;
- done;
- assert false
- with End_of_file ->
- Stdlib.close_in in_channel;
- Buffer.contents buf
- in
- let regexps_result =
- [ (string_valid_of_solver, Valid);
- (string_invalid_of_solver, Invalid);
- (string_timeout_of_solver, Timeout);
- (string_unknown_of_solver, Unknown); ]
- in
- List.fold
- regexps_result
- ~init:Failure
- ~f:(fun acc (f, result) ->
- let regexp = Str.regexp (f solver) in
- let found =
- try Str.search_forward regexp output 0 >= 0
- with Stdlib.Not_found -> false
- in
- if found
- then result
- else acc)
-
-let pretty_result fmt result =
- Format.fprintf fmt "%s" (String.uppercase (show_result result))
+module Format = Caml.Format
-let exec ~raw_options config model property =
- let open Result in
- (* Check solver availability. *)
- check_availability config >>= fun () ->
- (* Check solver and model compatibility. *)
- check_compatibility config model >>= fun () ->
- (* Build the required command-line. *)
- build_command ~raw_options config property model
- >>= fun (prop, cmd, (stdout, summary)) ->
- (* Execute the command. *)
- begin
- Logs.app (fun m ->
- m "Launching verification with `%a'." pp_solver config.solver);
- try
- Logs.info (fun m -> m "Executing command `%s'." cmd);
- let retcode = Sys.command cmd in
- Sys.remove prop;
- if retcode <> 0
- then
- Error (Format.sprintf "Command `%s' failed." cmd)
- else begin
- (* Extract and pretty-print verification result. *)
- let result = extract_result config stdout summary in
- Logs.app (fun m -> m "Result: %a." pretty_result result);
- if equal_result result Failure
- then Logs.app (fun m ->
- m "See error messages in `%s' for more information." stdout)
- else Sys.remove stdout;
- Option.value_map summary ~default:() ~f:Sys.remove;
- Ok ()
- end
- with _ ->
- Error "Unexpected failure."
- end
+module Result = struct
+ type t =
+ | Valid
+ | Invalid
+ | Timeout
+ | Unknown
+ | Failure
+ [@@deriving show { with_path = false }, eq]
+
+ let pretty fmt t =
+ Format.fprintf fmt "%s" (String.uppercase (show t))
+end
+
+(* Solver instances. *)
+
+module type S = sig
+ type t
+ val name: string
+ val exe_name: string
+ val exe_default_option: string
+ val re_version: Str.regexp
+ val re_of_result: Result.t -> Str.regexp
+ val is_model_format_supported: Model.format -> bool
+ val options: model:string -> property:string -> output:string -> string list
+ val consolidate: Result.t -> Result.t -> Result.t
+ val translate: hypothesis:formula -> goal:formula -> t
+ val repr: t -> formula list
+ val pretty: Caml.Format.formatter -> formula -> unit
+end
+
+type instance = (module S)
diff --git a/solver.mli b/solver.mli
index 6a70c6a..6934a70 100644
--- a/solver.mli
+++ b/solver.mli
@@ -4,28 +4,60 @@
(* *)
(**************************************************************************)
-(** Supported solvers. *)
-type solver = Pyrat | Marabou [@@deriving show]
+open Property_types
-(** The list of supported solvers by default. *)
-val defaults: solver list
+(** Solver possible results. *)
+module Result: sig
+ type t =
+ | Valid
+ | Invalid
+ | Timeout
+ | Unknown
+ | Failure
+ [@@deriving show, eq]
-val default_config_file: string
+ val pretty: Caml.Format.formatter -> t -> unit
+end
-(** [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
+(** Solvers common interface. *)
+module type S = sig
+ type t
-(** Solver configuration. *)
-type config
+ (** The name of the solver. *)
+ val name: string
-(** [get_config ~file solver] retrieves the [solver] configuration, if any, from
- the given [file]. *)
-val get_config: file:string -> solver -> (config, string) Result.t
+ (** The executable name. *)
+ val exe_name: string
-(** [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 list ->
- config -> Model.t -> Property.t -> (unit, string) Result.t
+ (** The default option of the executable. Typically, `--version'. *)
+ val exe_default_option: string
+
+ (** Regexp for extracting the solver version when running the solver on the
+ default option. *)
+ val re_version: Str.regexp
+
+ (** @return regexp for extracting the given result from the solver output. *)
+ val re_of_result: Result.t -> Str.regexp
+
+ (** @return whether the given model format is supported by the solver. *)
+ val is_model_format_supported: Model.format -> bool
+
+ (** @return solver options to execute the solver on the given [model] and
+ [property] files, while using [output] as file to store the result. *)
+ val options: model:string -> property:string -> output:string -> string list
+
+ (** @return consolidated result of the given ones. *)
+ val consolidate: Result.t -> Result.t -> Result.t
+
+ (** Encodes the given formulae into the solver internal representation. *)
+ val translate: hypothesis:formula -> goal:formula -> t
+
+ (** Decodes the internal representation into formulae. *)
+ val repr: t -> formula list
+
+ (** Solver pretty-printing of formulae. *)
+ val pretty: Caml.Format.formatter -> formula -> unit
+end
+
+(** An actual instance of solver interface [S]. *)
+type instance = (module S)
--
GitLab