diff --git a/src/dataset.ml b/src/dataset.ml
index 6ce481846cd19043eea6f79a4265e965fe684d8c..32dbe5af9dc5adc50546268a5277033e9dd90e9b 100644
--- a/src/dataset.ml
+++ b/src/dataset.ml
@@ -23,9 +23,27 @@
open Why3
open Base
+let real_constant_of_float value =
+ let neg = Float.is_negative value in
+ let value = Fmt.str "%.64f" (Float.abs value) in
+ (* Split into integer and fractional parts. *)
+ let int_frac = String.split value ~on:'.' in
+ let int = List.hd_exn int_frac in
+ let frac =
+ match List.tl_exn int_frac with
+ | [] -> ""
+ | [ s ] -> s
+ | _ -> assert false (* Since every float has one '.' at most. *)
+ in
+ Constant.ConstReal (Number.real_literal ~radix:10 ~neg ~int ~frac ~exp:None)
+
+let float_of_real_constant rc =
+ Float.of_string (Fmt.str "%a" Number.(print_real_constant full_support) rc)
+
type normalization =
| MinMax of float * float (* min-max scaling *)
| Znorm of float * float (* z-normalization (mean, standard deviation) *)
+[@@deriving yojson, show]
let require_clipping = function MinMax _ -> true | Znorm _ -> false
@@ -45,9 +63,6 @@ let apply_normalization csv ds =
class_ :: features)
let interpret_normalization =
- let float_of_real_constant rc =
- Float.of_string (Fmt.str "%a" Number.(print_real_constant full_support) rc)
- in
Trans.fold_decl
(fun decl acc ->
match decl.d_node with
@@ -83,12 +98,44 @@ let interpret_normalization =
| _ -> acc)
[]
-type eps = Constant.constant
+let term_of_normalization env normalization =
+ let th = Pmodule.read_module env [ "caisar" ] "DataSetClassification" in
+ let t_dataset =
+ let ls_dataset = Theory.ns_find_ls th.mod_theory.th_export [ "dataset" ] in
+ Term.t_app_infer ls_dataset []
+ in
+ let ty =
+ let th = Env.read_theory env [ "ieee_float" ] "Float64" in
+ Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) []
+ in
+ match normalization with
+ | MinMax (min, max) ->
+ let t_min = Term.t_const (real_constant_of_float min) ty in
+ let t_max = Term.t_const (real_constant_of_float max) ty in
+ let ls_min_max_scale =
+ Theory.ns_find_ls th.mod_theory.th_export [ "min_max_scale" ]
+ in
+ Term.t_app_infer ls_min_max_scale [ t_min; t_max; t_dataset ]
+ | Znorm (mean, std_dev) ->
+ let t_mean = Term.t_const (real_constant_of_float mean) ty in
+ let t_std_dev = Term.t_const (real_constant_of_float std_dev) ty in
+ let ls_z_norm = Theory.ns_find_ls th.mod_theory.th_export [ "z_norm" ] in
+ Term.t_app_infer ls_z_norm [ t_mean; t_std_dev; t_dataset ]
+
+type eps = float [@@deriving yojson, show]
+
+let string_of_eps eps = Float.to_string eps
+
+let term_of_eps env eps =
+ let th = Env.read_theory env [ "ieee_float" ] "Float64" in
+ let ty = Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) [] in
+ Term.t_const (real_constant_of_float eps) ty
type property =
| Correct
| Robust of eps
| CondRobust of eps
+[@@deriving yojson, show]
type ('a, 'b) predicate = {
model : 'a;
@@ -97,8 +144,6 @@ type ('a, 'b) predicate = {
property : property;
}
-let string_of_eps eps = Fmt.str "%a" Constant.print_def eps
-
let string_of_predicate_kind = function
| Correct -> "correct"
| Robust _ -> "robust"
@@ -131,13 +176,14 @@ let interpret_predicate env ~on_model ~on_dataset task =
if Term.ls_equal ls correct_predicate
then Correct
else failwith_unsupported_ls ls
- | [ { t_node = Tconst (Constant.ConstReal _ as e); _ } ] ->
+ | [ { t_node = Tconst (Constant.ConstReal e); _ } ] ->
let robust_predicate = find_predicate_ls env "robust" in
let cond_robust_predicate = find_predicate_ls env "cond_robust" in
+ let f = float_of_real_constant e in
if Term.ls_equal ls robust_predicate
- then Robust e
+ then Robust f
else if Term.ls_equal ls cond_robust_predicate
- then CondRobust e
+ then CondRobust f
else failwith_unsupported_ls ls
| _ -> failwith_unsupported_term term
in
@@ -157,19 +203,6 @@ let clip_value value =
let value = if Float.is_negative value then Float.zero else value in
if Float.(is_negative (one -. value)) then Float.one else value
-let real_constant value =
- (* Split into integer and fractional parts. *)
- let int_frac = String.split Float.(to_string (abs value)) ~on:'.' in
- let int = List.hd_exn int_frac in
- let frac =
- match List.tl_exn int_frac with
- | [] -> ""
- | [ s ] -> s
- | _ -> assert false (* Since every float has one '.' at most. *)
- in
- Constant.ConstReal
- (Number.real_literal ~radix:10 ~neg:false ~int ~frac ~exp:None)
-
let add_axioms ?eps ~clip th task input value =
let eps = Float.(abs (of_string (Option.value eps ~default:"0"))) in
let value = Float.of_string value in
@@ -182,7 +215,7 @@ let add_axioms ?eps ~clip th task input value =
let t_ge =
let value = value -. eps in
let value = if clip then clip_value value else value in
- let cst = real_constant value in
+ let cst = real_constant_of_float value in
Term.(ps_app le [ t_const cst Ty.ty_real; fs_app input [] Ty.ty_real ])
in
let task = Task.add_prop_decl task Decl.Paxiom pr_ge t_ge in
@@ -194,7 +227,7 @@ let add_axioms ?eps ~clip th task input value =
let t_le =
let value = value +. eps in
let value = if clip then clip_value value else value in
- let cst = real_constant value in
+ let cst = real_constant_of_float value in
Term.(ps_app le [ fs_app input [] Ty.ty_real; t_const cst Ty.ty_real ])
in
Task.add_prop_decl task Decl.Paxiom pr_le t_le
@@ -214,16 +247,16 @@ let add_output_decl ~id predicate_kind ~outputs ~record th task =
(* Add goal formula. *)
let class_ = List.hd_exn record in
let goal_fmla =
- let gt = Theory.(ns_find_ls th.th_export [ Ident.op_infix ">" ]) in
- let class_ls = List.nth_exn outputs (Int.of_string class_) in
+ let ls_gt = Theory.(ns_find_ls th.th_export [ Ident.op_infix ">" ]) in
+ let ls_class = List.nth_exn outputs (Int.of_string class_) in
List.fold outputs ~init:Term.t_true ~f:(fun fmla output ->
- if Term.ls_equal class_ls output
+ if Term.ls_equal ls_class output
then fmla
else
let gt_fmla =
Term.(
- ps_app gt
- [ fs_app class_ls [] Ty.ty_real; fs_app output [] Ty.ty_real ])
+ ps_app ls_gt
+ [ fs_app ls_class [] Ty.ty_real; fs_app output [] Ty.ty_real ])
in
Term.t_and fmla gt_fmla)
in
diff --git a/src/dataset.mli b/src/dataset.mli
index 5efbdb9b017720a70e2c04d9aa9bacc988bac23c..f1f2e13d9964cc986ef609f3595de91fa8860d96 100644
--- a/src/dataset.mli
+++ b/src/dataset.mli
@@ -22,14 +22,20 @@
open Why3
-type eps
+type eps [@@deriving yojson, show]
+
+val string_of_eps : eps -> string
+val term_of_eps : Env.env -> eps -> Term.term
type property = private
| Correct
| Robust of eps
| CondRobust of eps
+[@@deriving yojson, show]
+
+type normalization [@@deriving yojson, show]
-type normalization
+val term_of_normalization : Env.env -> normalization -> Term.term
type ('model, 'dataset) predicate = private {
model : 'model;
@@ -38,8 +44,6 @@ type ('model, 'dataset) predicate = private {
property : property;
}
-val string_of_eps : eps -> string
-
val interpret_predicate :
Env.env ->
on_model:(Term.lsymbol -> 'model) ->
diff --git a/src/language.ml b/src/language.ml
index b89e65b09a7d74e81d4e135aa0b16876e131d229..789d5bc6a2f101bd9e3267504dfd3b562424fa33 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -102,47 +102,56 @@ let register_svm_as_array env nb_inputs nb_classes filename mstr =
in
Wstdlib.Mstr.add name (Pmodule.close_module th_uc) mstr
-let nnet_parser env _ filename _ =
- let model = Nnet.parse ~permissive:true filename in
- match model with
- | Error s -> Loc.errorm "%s" s
- | Ok { n_inputs; n_outputs; _ } ->
- Wstdlib.Mstr.empty
- |> register_nn_as_tuple env n_inputs n_outputs filename
- |> register_nn_as_array env n_inputs n_outputs filename
+let nnet_parser =
+ Env.Wenv.memoize 13 (fun env ->
+ let h = Hashtbl.create (module String) in
+ Hashtbl.findi_or_add h ~default:(fun filename ->
+ let model = Nnet.parse ~permissive:true filename in
+ match model with
+ | Error s -> Loc.errorm "%s" s
+ | Ok { n_inputs; n_outputs; _ } ->
+ Wstdlib.Mstr.empty
+ |> register_nn_as_tuple env n_inputs n_outputs filename
+ |> register_nn_as_array env n_inputs n_outputs filename))
-let onnx_parser env _ filename _ =
- let model = Onnx.parse filename in
- match model with
- | Error s -> Loc.errorm "%s" s
- | Ok { n_inputs; n_outputs; nier } ->
- let nier =
- match nier with
- | Error msg ->
- Logs.warn (fun m ->
- m "Cannot build network intermediate representation:@ %s" msg);
- None
- | Ok nier -> Some nier
- in
- Wstdlib.Mstr.empty
- |> register_nn_as_tuple env n_inputs n_outputs filename ?nier
- |> register_nn_as_array env n_inputs n_outputs filename ?nier
+let onnx_parser =
+ Env.Wenv.memoize 13 (fun env ->
+ let h = Hashtbl.create (module String) in
+ Hashtbl.findi_or_add h ~default:(fun filename ->
+ let model = Onnx.parse filename in
+ match model with
+ | Error s -> Loc.errorm "%s" s
+ | Ok { n_inputs; n_outputs; nier } ->
+ let nier =
+ match nier with
+ | Error msg ->
+ Logs.warn (fun m ->
+ m "Cannot build network intermediate representation:@ %s" msg);
+ None
+ | Ok nier -> Some nier
+ in
+ Wstdlib.Mstr.empty
+ |> register_nn_as_tuple env n_inputs n_outputs filename ?nier
+ |> register_nn_as_array env n_inputs n_outputs filename ?nier))
-let ovo_parser env _ filename _ =
- let model = Ovo.parse filename in
- match model with
- | Error s -> Loc.errorm "%s" s
- | Ok { n_inputs; n_outputs } ->
- register_svm_as_array env n_inputs n_outputs filename Wstdlib.Mstr.empty
+let ovo_parser =
+ Env.Wenv.memoize 13 (fun env ->
+ let h = Hashtbl.create (module String) in
+ Hashtbl.findi_or_add h ~default:(fun filename ->
+ let model = Ovo.parse filename in
+ match model with
+ | Error s -> Loc.errorm "%s" s
+ | Ok { n_inputs; n_outputs } ->
+ register_svm_as_array env n_inputs n_outputs filename Wstdlib.Mstr.empty))
let register_nnet_support () =
Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language
- "NNet" [ "nnet" ] nnet_parser
+ "NNet" [ "nnet" ] (fun env _ filename _ -> nnet_parser env filename)
let register_onnx_support () =
Env.register_format ~desc:"ONNX format" Pmodule.mlw_language "ONNX" [ "onnx" ]
- onnx_parser
+ (fun env _ filename _ -> onnx_parser env filename)
let register_ovo_support () =
Env.register_format ~desc:"OVO format" Pmodule.mlw_language "OVO" [ "ovo" ]
- ovo_parser
+ (fun env _ filename _ -> ovo_parser env filename)
diff --git a/src/language.mli b/src/language.mli
index 39453b44cd27434478bda373e22b03cc8955026e..68c71572b844dc0aff4a1578be3d999950cad000 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -50,3 +50,15 @@ val register_onnx_support : unit -> unit
val register_ovo_support : unit -> unit
(** Register OVO parser. *)
+
+val nnet_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t
+(* [nnet_parser env filename] parses and creates the theories corresponding to
+ the given nnet [filename]. The result is memoized. *)
+
+val onnx_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t
+(* [onnx_parser env filename] parses and creates the theories corresponding to
+ the given onnx [filename]. The result is memoized. *)
+
+val ovo_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t
+(* [nnet_parser env filename] parses and creates the theories corresponding to
+ the given ovo [filename]. The result is memoized. *)
diff --git a/src/main.ml b/src/main.ml
index 35fcd65082e735f31a4595e2ca3eee658b94bbd5..c59b9740df57988f8f391843a1640aab3441af4f 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -102,7 +102,7 @@ let memlimit_of_string s =
| [ v ], ([] | [ "M" ] | [ "MB" ]) -> Int.of_string v
| [ v ], ([ "G" ] | [ "GB" ]) -> Int.of_string v * 1000
| [ v ], ([ "T" ] | [ "TB" ]) -> Int.of_string v * 1000000
- | _ -> failwith "Unrecognized memory limit"
+ | _ -> invalid_arg "Unrecognized memory limit"
let timelimit_of_string s =
let s = String.strip s in
@@ -118,18 +118,25 @@ let timelimit_of_string s =
| [ v ], ([] | [ "s" ]) -> Int.of_string v
| [ v ], [ "m" ] -> Int.of_string v * 60
| [ v ], [ "h" ] -> Int.of_string v * 3600
- | _ -> failwith "Unrecognized time limit"
+ | _ -> invalid_arg "Unrecognized time limit"
-let verify format loadpath memlimit timelimit prover dataset_csv files =
+let verify ?format ~loadpath ?memlimit ?timelimit prover ?dataset_csv files =
let debug = log_level_is_debug () in
let memlimit = Option.map memlimit ~f:memlimit_of_string in
let timelimit = Option.map timelimit ~f:timelimit_of_string in
List.iter
~f:
- (Verification.verify ~debug format loadpath ?memlimit ?timelimit prover
+ (Verification.verify ~debug ?format ~loadpath ?memlimit ?timelimit prover
?dataset_csv)
files
+let verify_json ?memlimit ?timelimit file =
+ let jc = Result.ok_exn (Verification.JSON.of_string file) in
+ let prover = jc.Verification.JSON.prover in
+ let dataset_csv = jc.Verification.JSON.property.dataset in
+ let file = Result.ok_or_failwith (Verification.File.of_json_config jc) in
+ verify ~loadpath:[] ?memlimit ?timelimit prover ~dataset_csv [ file ]
+
let exec_cmd cmdname cmd =
Logs.debug (fun m -> m "Command `%s'" cmdname);
cmd ()
@@ -158,7 +165,7 @@ let config_cmd =
ret
(const (fun detect _ ->
if not detect
- then `Help (`Pager, Some "config")
+ then `Help (`Pager, Some cmdname)
else
(* TODO: Do not only check for [detect], and enable it by default,
as soon as other options are available. *)
@@ -167,47 +174,43 @@ let config_cmd =
in
Cmd.v info term
+let memlimit =
+ let doc =
+ "Memory limit. $(docv) is intended in megabytes (MB) by default, but \
+ gigabytes (GB) and terabytes (TB) may also be specified instead."
+ in
+ Arg.(
+ value & opt (some string) None & info [ "m"; "memlimit" ] ~doc ~docv:"MEM")
+
+let timelimit =
+ let doc =
+ "Time limit. $(docv) is intended in seconds (s) by default, but minutes \
+ (m) and hours (h) may also be specified instead."
+ in
+ Arg.(
+ value & opt (some string) None & info [ "t"; "timelimit" ] ~doc ~docv:"TIME")
+
let verify_cmd =
let cmdname = "verify" in
- let doc = "Property verification using external provers." in
let info =
+ let doc = "Property verification using external provers." in
Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits:Cmd.Exit.defaults
~doc
~man:[ `S Manpage.s_description; `P doc ]
in
+ let loadpath =
+ let doc = "Additional loadpath." in
+ Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
+ in
+ let format =
+ let doc = "File format." in
+ Arg.(value & opt (some string) None & info [ "format" ] ~doc)
+ in
let term =
let files =
- let doc = "Files to verify." in
- let file_or_stdin = Verification.File.(of_string, pretty) in
- Arg.(value & pos_all file_or_stdin [] & info [] ~doc)
- in
- let format =
- let doc = "File format." in
- Arg.(value & opt (some string) None & info [ "format" ] ~doc)
- in
- let loadpath =
- let doc = "Additional loadpath." in
- Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
- in
- let memlimit =
- let doc =
- "Memory limit. $(docv) is intended in megabytes (MB) by default, but \
- gigabytes (GB) and terabytes (TB) may also be specified instead."
- in
- Arg.(
- value
- & opt (some string) None
- & info [ "m"; "memlimit" ] ~doc ~docv:"MEM")
- in
- let timelimit =
- let doc =
- "Time limit. $(docv) is intended in seconds (s) by default, but \
- minutes (m) and hours (h) may also be specified instead."
- in
- Arg.(
- value
- & opt (some string) None
- & info [ "t"; "timelimit" ] ~doc ~docv:"TIME")
+ let doc = "File to verify." in
+ let file_or_stdin = Arg.conv' Verification.File.(of_string, pretty) in
+ Arg.(non_empty & pos_all file_or_stdin [] & info [] ~doc ~docv:"FILE")
in
let prover =
let all_provers = Prover.list_available () in
@@ -227,15 +230,37 @@ let verify_cmd =
Arg.(value & opt (some file) None & info [ "dataset-csv" ] ~doc)
in
Term.(
- ret
- (const
- (fun format loadpath memlimit timelimit prover dataset_csv files _ ->
- `Ok
- (exec_cmd cmdname (fun () ->
- verify format loadpath memlimit timelimit prover dataset_csv
- files)))
- $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset_csv
- $ files $ setup_logs))
+ const
+ (fun format loadpath memlimit timelimit prover dataset_csv files _ ->
+ exec_cmd cmdname (fun () ->
+ verify ?format ~loadpath ?memlimit ?timelimit prover ?dataset_csv
+ files))
+ $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset_csv $ files
+ $ setup_logs)
+ in
+ Cmd.v info term
+
+let verify_json_cmd =
+ let cmdname = "verify-json" in
+ let info =
+ let doc =
+ "Property verification using external provers via json configuration \
+ file."
+ in
+ Cmd.info cmdname ~sdocs:Manpage.s_common_options ~exits:Cmd.Exit.defaults
+ ~doc
+ ~man:[ `S Manpage.s_description; `P doc ]
+ in
+ let term =
+ let json =
+ let doc = "JSON file." in
+ Arg.(
+ required & pos ~rev:true 0 (some file) None & info [] ~doc ~docv:"FILE")
+ in
+ Term.(
+ const (fun memlimit timelimit json _ ->
+ exec_cmd cmdname (fun () -> verify_json ?memlimit ?timelimit json))
+ $ memlimit $ timelimit $ json $ setup_logs)
in
Cmd.v info term
@@ -272,7 +297,8 @@ let () =
let () =
try
- Cmd.group ~default:default_cmd default_info [ config_cmd; verify_cmd ]
+ Cmd.group ~default:default_cmd default_info
+ [ config_cmd; verify_cmd; verify_json_cmd ]
|> Cmd.eval ~catch:false |> Caml.exit
with exn when not (log_level_is_debug ()) ->
Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)
diff --git a/src/prover.ml b/src/prover.ml
index 517d4f447504bdac64e80191001cff15679417b1..847cc3e20e0896f11deb8cf00cf636834185642a 100644
--- a/src/prover.ml
+++ b/src/prover.ml
@@ -25,6 +25,7 @@ type t =
| Pyrat
| Saver
| CVC5
+[@@deriving yojson, show]
let list_available () = [ Marabou; Pyrat; Saver; CVC5 ]
diff --git a/src/prover.mli b/src/prover.mli
index 36ddf1a72a47776dc3ec2322a3359fed09011af2..1ae811a671fa5d950f8c60f1f9baa0bfd4d9192d 100644
--- a/src/prover.mli
+++ b/src/prover.mli
@@ -25,6 +25,7 @@ type t = private
| Pyrat
| Saver
| CVC5
+[@@deriving yojson, show]
val list_available : unit -> t list
val of_string : string -> t option
diff --git a/src/verification.ml b/src/verification.ml
index 71728ea3122517fc51a02e4db18b4e0c4ec62b63..fa183c52c83c0b68ba0352589c91cb6dd234692c 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -24,21 +24,142 @@ open Why3
open Base
module Filename = Caml.Filename
+module JSON = struct
+ type t = {
+ prover : Prover.t;
+ model : string;
+ property : property;
+ }
+ [@@deriving yojson, show]
+
+ and property = {
+ dataset : string;
+ normalization : Dataset.normalization option;
+ kind : Dataset.property;
+ }
+ [@@deriving yojson, show]
+
+ let of_string s =
+ match of_yojson (Yojson.Safe.from_file s) with
+ | Ok t -> Ok t
+ | Error msg ->
+ Error
+ (invalid_arg
+ (Fmt.str "Unrecognized JSON configuration in file '%s' (%s)" s msg))
+ | exception Yojson.Json_error msg ->
+ Error
+ (failwith
+ (Fmt.str "Unexpected error while parsing JSON file '%s' (%s)" s msg))
+
+ let pretty fmt t = Fmt.fmt "%a" fmt pp t
+
+ let mstr_theory_of_json env t =
+ let th_as_array =
+ let model_parser =
+ let extension = Filename.(extension (basename t.model)) in
+ match String.lowercase extension with
+ | ".nnet" -> Language.nnet_parser
+ | ".onnx" -> Language.onnx_parser
+ | ".ovo" -> Language.ovo_parser
+ | "" -> invalid_arg "Cannot find model file extension"
+ | _ ->
+ invalid_arg (Fmt.str "Unrecognized model extension '%s'" extension)
+ in
+ let pmod = model_parser env (Unix.realpath t.model) in
+ (Wstdlib.Mstr.find "AsArray" pmod).mod_theory
+ in
+ let th_float64 = Env.read_theory env [ "ieee_float" ] "Float64" in
+ let th_ds_classification =
+ Pmodule.read_module env [ "caisar" ] "DataSetClassification"
+ in
+ let th_ds_props = Pmodule.read_module env [ "caisar" ] "DataSetProps" in
+ let name = "JSON" in
+ let th_uc = Theory.create_theory (Ident.id_fresh name) in
+ let th_uc = Theory.use_export th_uc th_as_array in
+ let th_uc = Theory.use_export th_uc th_float64 in
+ let th_uc = Theory.use_export th_uc th_ds_classification.mod_theory in
+ let th_uc = Theory.use_export th_uc th_ds_props.mod_theory in
+ let t_dataset =
+ let ls_dataset =
+ Theory.ns_find_ls th_ds_classification.mod_theory.th_export
+ [ "dataset" ]
+ in
+ Term.t_app_infer ls_dataset []
+ in
+ let t_model =
+ let ls_model = Theory.ns_find_ls th_as_array.th_export [ "model" ] in
+ Term.t_app_infer ls_model []
+ in
+ (* Add dataset normalization. *)
+ let t_dataset, th_uc =
+ match t.property.normalization with
+ | None -> (t_dataset, th_uc)
+ | Some n ->
+ let t_normalization = Dataset.term_of_normalization env n in
+ let ls_dataset_norm =
+ let ty =
+ Ty.ty_app
+ (Theory.ns_find_ts th_ds_classification.mod_theory.th_export
+ [ "dataset" ])
+ []
+ in
+ Term.create_fsymbol (Ident.id_fresh "dataset'") [] ty
+ in
+ let ld_dataset_norm =
+ Decl.make_ls_defn ls_dataset_norm [] t_normalization
+ in
+ ( Term.t_app_infer ls_dataset_norm [],
+ Theory.add_logic_decl th_uc [ ld_dataset_norm ] )
+ in
+ (* Create goal formula about specified property. *)
+ let th_uc =
+ let t_property =
+ match t.property.kind with
+ | Dataset.Correct ->
+ let ls_correct =
+ Theory.ns_find_ls th_ds_props.mod_theory.th_export [ "correct" ]
+ in
+ Term.t_app_infer ls_correct [ t_model; t_dataset ]
+ | Robust eps ->
+ let ls_robust =
+ Theory.ns_find_ls th_ds_props.mod_theory.th_export [ "robust" ]
+ in
+ let t_eps = Dataset.term_of_eps env eps in
+ Term.t_app_infer ls_robust [ t_model; t_dataset; t_eps ]
+ | CondRobust _ -> invalid_arg "Not yet supported property"
+ in
+ let prsymbol = Decl.create_prsymbol (Ident.id_fresh "property") in
+ Theory.add_prop_decl th_uc Decl.Pgoal prsymbol t_property
+ in
+ let th = Theory.close_theory th_uc in
+ Wstdlib.Mstr.singleton name th
+end
+
module File = struct
type t =
| Stdin
| File of string
+ | Json of JSON.t
+
+ let of_json_config jc =
+ if Caml.Sys.file_exists jc.JSON.model
+ then
+ if Caml.Sys.file_exists jc.JSON.property.dataset
+ then Ok (Json jc)
+ else Error (Fmt.str "no '%s' file or directory" jc.property.dataset)
+ else Error (Fmt.str "no '%s' file or directory" jc.model)
let of_string s =
if String.equal s "-"
- then `Ok Stdin
+ then Ok Stdin
else if Caml.Sys.file_exists s
- then `Ok (File s)
- else `Error (Fmt.str "no '%s' file or directory" s)
+ then Ok (File s)
+ else Error (Fmt.str "no '%s' file or directory" s)
let pretty fmt = function
| Stdin -> Fmt.string fmt "-"
| File f -> Fmt.string fmt f
+ | Json j -> JSON.pretty fmt j
end
let () =
@@ -173,7 +294,7 @@ let call_prover ~limit config env prover config_prover driver dataset_csv task =
Fmt.(option ~none:nop (any " " ++ string))
additional_info)
-let verify ?(debug = false) format loadpath ?memlimit ?timelimit prover
+let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit prover
?dataset_csv file =
if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
let env, config = create_env ~debug loadpath in
@@ -188,13 +309,14 @@ let verify ?(debug = false) format loadpath ?memlimit ?timelimit prover
Call_provers.limit_mem = memlimit;
}
in
- let _, mstr_theory =
+ let mstr_theory =
match file with
| File.Stdin ->
- ("stdin", Env.(read_channel ?format base_language env "stdin" Caml.stdin))
+ Env.(read_channel ?format base_language env "stdin" Caml.stdin)
| File file ->
let mlw_files, _ = Env.(read_file ?format base_language env file) in
- (file, mlw_files)
+ mlw_files
+ | Json json -> JSON.mstr_theory_of_json env json
in
Wstdlib.Mstr.iter
(fun _ theory ->
diff --git a/src/verification.mli b/src/verification.mli
index 6bfed09d04491523e4d732c8649f637d93a8ea1d..5572343a325c553d6cfcc4bfc52a63fc4cfeb585 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -20,17 +20,37 @@
(* *)
(**************************************************************************)
+module JSON : sig
+ type t = private {
+ prover : Prover.t;
+ model : string;
+ property : property;
+ }
+ [@@deriving yojson, show]
+
+ and property = private {
+ dataset : string;
+ normalization : Dataset.normalization option;
+ kind : Dataset.property;
+ }
+ [@@deriving yojson, show]
+
+ val of_string : string -> (t, exn) result
+ val pretty : Format.formatter -> t -> unit
+end
+
module File : sig
type t
- val of_string : string -> [ `Ok of t | `Error of string ]
+ val of_json_config : JSON.t -> (t, string) result
+ val of_string : string -> (t, string) result
val pretty : Format.formatter -> t -> unit
end
val verify :
?debug:bool ->
- string option ->
- string list ->
+ ?format:string ->
+ loadpath:string list ->
?memlimit:int ->
?timelimit:int ->
Prover.t ->
diff --git a/tests/pyrat_verify_json.t b/tests/pyrat_verify_json.t
new file mode 100644
index 0000000000000000000000000000000000000000..aace62695510d7b4b8a40b3c1348795d35f2bd70
--- /dev/null
+++ b/tests/pyrat_verify_json.t
@@ -0,0 +1,18 @@
+Test verify-json
+ $ cat - > test_data.csv << EOF
+ > 1,0,255,200,5,198
+ > EOF
+
+ $ cat - > config.json << EOF
+ > {"prover":["Pyrat"],"model":"TestNetwork.nnet","property":{"dataset":"test_data.csv","normalization":["MinMax",0.0,255.0],"kind":["Robust",0.01]}}
+ > EOF
+
+ $ chmod u+x bin/pyrat.py
+
+ $ bin/pyrat.py --version
+ PyRAT 1.1
+
+ $ PATH=$(pwd)/bin:$PATH
+
+ $ caisar verify-json config.json 2>&1 <<EOF | ./filter_tmpdir.sh
+ [caisar] Goal property: Unknown ()