diff --git a/src/dataset.ml b/src/dataset.ml
index 6ce481846cd19043eea6f79a4265e965fe684d8c..456981ec3794394be178be1b57ce9f50d6ca7cbb 100644
--- a/src/dataset.ml
+++ b/src/dataset.ml
@@ -23,9 +23,13 @@
open Why3
open Base
+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 +49,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 +84,13 @@ let interpret_normalization =
| _ -> acc)
[]
-type eps = Constant.constant
+type eps = float [@@deriving yojson, show]
type property =
| Correct
| Robust of eps
| CondRobust of eps
+[@@deriving yojson, show]
type ('a, 'b) predicate = {
model : 'a;
@@ -97,7 +99,7 @@ type ('a, 'b) predicate = {
property : property;
}
-let string_of_eps eps = Fmt.str "%a" Constant.print_def eps
+let string_of_eps eps = Float.to_string eps
let string_of_predicate_kind = function
| Correct -> "correct"
@@ -131,13 +133,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
diff --git a/src/dataset.mli b/src/dataset.mli
index 5efbdb9b017720a70e2c04d9aa9bacc988bac23c..e1465f7bf029ec4d2adff8386e6263dff225490d 100644
--- a/src/dataset.mli
+++ b/src/dataset.mli
@@ -22,14 +22,15 @@
open Why3
-type eps
+type eps [@@deriving yojson, show]
type property = private
| Correct
| Robust of eps
| CondRobust of eps
+[@@deriving yojson, show]
-type normalization
+type normalization [@@deriving yojson, show]
type ('model, 'dataset) predicate = private {
model : 'model;
diff --git a/src/main.ml b/src/main.ml
index 6b22ab77bc2553b58b3faecdc3ff0000641fb1b9..42ae008f8d195cb3dca6c7ca264a7c207226c0a3 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -130,6 +130,33 @@ let verify format loadpath memlimit timelimit prover dataset_csv files =
?dataset_csv)
files
+let verify_json format loadpath memlimit timelimit file =
+ let json_config =
+ match
+ Verification.File.json_config_of_yojson (Yojson.Safe.from_file file)
+ with
+ | Ok json_config -> json_config
+ | Error msg ->
+ invalid_arg
+ (Fmt.str "Unrecognized JSON configuration in file '%s' (%s)" file msg)
+ | exception Yojson.Json_error msg ->
+ failwith
+ (Fmt.str "Unexpected error while parsing JSON file '%s' (%s)" file msg)
+ in
+ let dataset_csv =
+ (* The call to [verify] assumes [dataset_csv] to exist. For the [verify_cmd]
+ case, this property is ensured by the Cmdliner [file] converter. Here,
+ since the dataset string is inside a json, we need to perform such
+ checking by hand. *)
+ if Caml.Sys.file_exists json_config.property.dataset
+ then Some json_config.property.dataset
+ else
+ failwith
+ (Fmt.str "No '%s' file or directory" json_config.property.dataset)
+ in
+ verify format loadpath memlimit timelimit json_config.prover dataset_csv
+ [ Verification.File.of_json_config json_config ]
+
let exec_cmd cmdname cmd =
Logs.debug (fun m -> m "Command `%s'" cmdname);
cmd ()
@@ -232,6 +259,31 @@ let verify_cmd =
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 format loadpath memlimit timelimit json _ ->
+ exec_cmd cmdname (fun () ->
+ verify_json format loadpath memlimit timelimit json))
+ $ format $ loadpath $ memlimit $ timelimit $ json $ setup_logs)
+ in
+ Cmd.v info term
+
let default_info =
let doc =
"A platform for characterizing the safety and robustness of artificial \
@@ -265,7 +317,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 47f418bef37c0eca9ef9fb589accc25d3f4c0bd7..eeef52de9d03823cb31d6477add9fd9d09dd3700 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -25,9 +25,26 @@ open Base
module Filename = Caml.Filename
module File = struct
+ type json_config = {
+ prover : Prover.t;
+ model : string;
+ property : property;
+ }
+ [@@deriving yojson, show]
+
+ and property = {
+ dataset : string;
+ normalization : Dataset.normalization list;
+ kind : Dataset.property;
+ }
+ [@@deriving yojson, show]
+
type t =
| Stdin
| File of string
+ | Json of json_config
+
+ let of_json_config json = Json json
let of_string s =
if String.equal s "-"
@@ -39,6 +56,7 @@ module File = struct
let pretty fmt = function
| Stdin -> Fmt.string fmt "-"
| File f -> Fmt.string fmt f
+ | Json j -> Fmt.fmt "%a" fmt pp_json_config j
end
let () =
@@ -173,6 +191,13 @@ let call_prover ~limit config env prover config_prover driver dataset_csv task =
Fmt.(option ~none:nop (any " " ++ string))
additional_info)
+let mstr_theory_of_json_config env _json_config =
+ let name = "T" in
+ let th_uc = Theory.create_theory (Ident.id_fresh name) in
+ let th_real = Env.read_theory env [ "real" ] "Real" in
+ let th_uc = Theory.use_export th_uc th_real in
+ Wstdlib.Mstr.singleton name (Theory.close_theory th_uc)
+
let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit prover
?dataset_csv file =
if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
@@ -188,13 +213,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_config -> mstr_theory_of_json_config env json_config
in
Wstdlib.Mstr.iter
(fun _ theory ->
diff --git a/src/verification.mli b/src/verification.mli
index f71abad2969244b51e4d7a3e9ed0b902273cff41..73d527396860e6653c5812552954c5951833b8d5 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -21,8 +21,23 @@
(**************************************************************************)
module File : sig
+ type json_config = private {
+ prover : Prover.t;
+ model : string;
+ property : property;
+ }
+ [@@deriving yojson, show]
+
+ and property = private {
+ dataset : string;
+ normalization : Dataset.normalization list;
+ kind : Dataset.property;
+ }
+ [@@deriving yojson, show]
+
type t
+ val of_json_config : json_config -> t
val of_string : string -> [ `Ok of t | `Error of string ]
val pretty : Format.formatter -> t -> unit
end