Skip to content
Snippets Groups Projects
Commit 552e56a0 authored by Michele Alberti's avatar Michele Alberti
Browse files

Rework query API.

parent cc169034
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/main.ml
+ 14
− 66
View file @ 552e56a0
......@@ -79,38 +79,6 @@ let config detect () =
Whyconf.print_prover Pp.nothing)
provers))
let memlimit_of_string s =
let s = String.strip s in
let value =
let re = Re__.Pcre.regexp "[0-9]+" in
Re__.Core.matches re s
in
let unit =
let re = Re__.Pcre.regexp "MB?|GB?|TB?" in
Re__.Core.matches re s
in
match (value, unit) with
| [ v ], ([] | [ "M" ] | [ "MB" ]) -> Int.of_string v
| [ v ], ([ "G" ] | [ "GB" ]) -> Int.of_string v * 1000
| [ v ], ([ "T" ] | [ "TB" ]) -> Int.of_string v * 1000000
| _ -> Logging.user_error (fun m -> m "Unrecognized memory limit")
let timelimit_of_string s =
let s = String.strip s in
let value =
let re = Re__.Pcre.regexp "[0-9]+" in
Re__.Core.matches re s
in
let unit =
let re = Re__.Pcre.regexp "[a-z]" in
Re__.Core.matches re s
in
match (value, unit) with
| [ v ], ([] | [ "s" ]) -> Int.of_string v
| [ v ], [ "m" ] -> Int.of_string v * 60
| [ v ], [ "h" ] -> Int.of_string v * 3600
| _ -> Logging.user_error (fun m -> m "Unrecognized time limit")
let log_theory_answer =
Why3.Wstdlib.Mstr.iter (fun theory_name task_answers ->
Logs.info (fun m ->
......@@ -139,18 +107,15 @@ let log_theory_answer =
additional_info)))
let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
?definitions ?theories ?goals ?onnx_out_dir ?output_file ?query_name files =
let memory_limit = Option.map memlimit ~f:memlimit_of_string in
let time_limit = Option.map timelimit ~f:timelimit_of_string in
let id_query = Option.value query_name ~default:"CAISAR_verification" in
?definitions ?theories ?goals ?onnx_out_dir files =
let open Verification_types in
let problems =
List.map files ~f:(Problem.of_file ?definitions ?goals ?theories)
in
let queries =
List.map problems ~f:(fun problem ->
Query.make ~id:id_query prover problem ~prover_altern ~loadpath
~time_limit ~memory_limit ~onnx_out_dir ~dataset ~output_file)
Query.make ?prover_altern ~loadpath ?memlimit ?timelimit ?onnx_out_dir
?dataset prover problem)
in
let theory_answers = List.map queries ~f:(Verification.verify ?format) in
List.iter theory_answers ~f:log_theory_answer;
......@@ -177,38 +142,21 @@ let record_verification_result verification_result file =
verification_result
let verify_json ?memlimit ?timelimit ?outfile json =
let query = Verification_types.Query.of_json json in
let query =
(* Precedence to the command line option, if any. *)
(* TODO: * get proper default value instead of defining it twice in
verification.ml and here *)
match memlimit with
| None -> query
| Some m -> { query with memory_limit = Some (memlimit_of_string m) }
Verification_types.Query.of_json ?memlimit ?timelimit ?outfile json
in
let query =
(* Precedence to the command line option, if any. *)
match timelimit with
| None -> query
| Some t -> { query with time_limit = Some (timelimit_of_string t) }
in
let record_outfile results outfile =
(* Precedence to the command line option, if any. *)
match outfile with
| Some outfile -> record_verification_result results outfile
| None -> (
match query.output_file with
| Some f -> record_verification_result results f
| None ->
Logging.user_error (fun m ->
m
"@[Must specify an output file when verifying a property via the \
JSON API@]"))
in
let verification_results = Verification.verify ~format:"whyml" query in
record_outfile verification_results outfile
let verification_results = Verification.verify query in
let outfile =
match query.output_file with
| None ->
Logging.code_error ~src:Logs.default (fun m ->
m "No output file found to record verification results")
| Some outfile -> outfile
in
record_verification_result verification_results outfile
let verify_xgboost ?memlimit ?timelimit xgboost dataset prover =
let open Verification_types.Query in
let memlimit = Option.map memlimit ~f:memlimit_of_string in
let timelimit = Option.map timelimit ~f:timelimit_of_string in
Convert_xgboost.verify ?memlimit ?timelimit ~xgboost ~dataset ~prover ()
......
src/verification_types.ml
+ 73
− 12
View file @ 552e56a0
......@@ -74,12 +74,47 @@ module Query = struct
}
[@@deriving of_yojson { strict = false }, show]
let make ~id prover ~prover_altern problem ~loadpath ~time_limit ~memory_limit
~onnx_out_dir ~dataset ~output_file =
let memlimit_of_string s =
let s = String.strip s in
let value =
let re = Re__.Pcre.regexp "[0-9]+" in
Re__.Core.matches re s
in
let unit =
let re = Re__.Pcre.regexp "MB?|GB?|TB?" in
Re__.Core.matches re s
in
match (value, unit) with
| [ v ], ([] | [ "M" ] | [ "MB" ]) -> Int.of_string v
| [ v ], ([ "G" ] | [ "GB" ]) -> Int.of_string v * 1000
| [ v ], ([ "T" ] | [ "TB" ]) -> Int.of_string v * 1000000
| _ -> Logging.user_error (fun m -> m "Unrecognized memory limit")
let timelimit_of_string s =
let s = String.strip s in
let value =
let re = Re__.Pcre.regexp "[0-9]+" in
Re__.Core.matches re s
in
let unit =
let re = Re__.Pcre.regexp "[a-z]" in
Re__.Core.matches re s
in
match (value, unit) with
| [ v ], ([] | [ "s" ]) -> Int.of_string v
| [ v ], [ "m" ] -> Int.of_string v * 60
| [ v ], [ "h" ] -> Int.of_string v * 3600
| _ -> Logging.user_error (fun m -> m "Unrecognized time limit")
let make ~loadpath ?memlimit ?timelimit ?onnx_out_dir ?dataset prover
?prover_altern problem =
let id = "caisar_verification_query" in
let id =
Int.incr id_int;
id ^ Int.to_string !id_int
in
let memory_limit = Option.map memlimit ~f:memlimit_of_string in
let time_limit = Option.map timelimit ~f:timelimit_of_string in
{
id;
prover;
......@@ -89,19 +124,45 @@ module Query = struct
problem;
memory_limit;
onnx_out_dir;
output_file;
output_file = None;
dataset;
}
let of_json s =
match of_yojson (Yojson.Safe.from_file s) with
| Ok t -> t
| Error msg ->
invalid_arg
(Fmt.str "Unrecognized JSON configuration in file '%s' (%s)" s msg)
| exception Yojson.Json_error msg ->
failwith
(Fmt.str "Unexpected error while parsing JSON file '%s' (%s)" s msg)
let of_json ?memlimit ?timelimit ?outfile s =
let query =
match of_yojson (Yojson.Safe.from_file s) with
| Ok t -> t
| Error msg ->
invalid_arg
(Fmt.str "Unrecognized JSON configuration in file '%s' (%s)" s msg)
| exception Yojson.Json_error msg ->
failwith
(Fmt.str "Unexpected error while parsing JSON file '%s' (%s)" s msg)
in
let query =
(* Precedence to the command line option, if any. *)
(* TODO: get proper default value instead of defining it twice in
verification.ml and here *)
match memlimit with
| None -> query
| Some m -> { query with memory_limit = Some (memlimit_of_string m) }
in
let query =
(* Precedence to the command line option, if any. *)
match timelimit with
| None -> query
| Some t -> { query with time_limit = Some (timelimit_of_string t) }
in
match outfile with
| None -> (
match query.output_file with
| Some _ -> query
| None ->
Logging.user_error (fun m ->
m
"@[No output file while creating verification query from JSON \
file@]"))
| Some _ as output_file -> { query with output_file }
let pretty fmt = Fmt.fmt "%a" fmt pp
end
......
src/verification_types.mli
+ 37
− 37
View file @ 552e56a0
......@@ -51,7 +51,14 @@ module Problem : sig
File.t ->
t
(** [of_file defs goals file] builds a {!Problem.t} to be fed with a query to
CAISAR. *)
CAISAR.
@param definitions is a key:value list defining toplevel constants.
@param theories
identifies the theories whose goals are the only ones to verify.
@param goals
is a theory:goals list each identifying only the goals of a theory to
verify. *)
end
module Query : sig
......@@ -69,55 +76,48 @@ module Query : sig
}
[@@deriving of_yojson { strict = false }, show]
val pretty : Format.formatter -> t -> unit
val make :
id:string ->
loadpath:string list ->
?memlimit:string ->
?timelimit:string ->
?onnx_out_dir:string ->
?dataset:string ->
Prover.t ->
prover_altern:string option ->
?prover_altern:string ->
Problem.t ->
loadpath:string list ->
time_limit:int option ->
memory_limit:int option ->
onnx_out_dir:string option ->
dataset:string option ->
output_file:string option ->
t
(** [make id prover prover_altern problem loadpath problem time_limit memory_limit onnx_out_dir dataset output_file]
creates a valid verification query.
(** [make id loadpath problem time_limit memory_limit onnx_out_dir dataset output_file prover prover_altern problem]
creates a verification query.
@param id
is a string name of the verification query. Unspecified behaviour if
several queries share the same name.
@param prover is the {!Prover.t} for the verification query.
@param prover_altern
is an optional alternative [prover] configuration, as specified in the
file `caisar_detection.conf`.
@param problem is a {!Problem.t} value
@param loadpath
is the additional loadpath where CAISAR will look to resolve files.
@param time_limit
is the timeout (in seconds) granted to the verification. Default value:
20.
@param memory_limit
is the memory limit (in megabytes) granted to the verification. Default
value: 1000.
@param definitions is a key:value list defining toplevel constants.
@param theories
identifies the theories whose goals are the only ones to verify.
@param goals
is a theory:goals list each identifying only the goals of a theory to
verify.
@param memlimit is the memory limit granted to the verification.
@param timelimit is the timeout granted to the verification.
@param onnx_out_dir
is the directory in which to write the ONNX files generated from the
NIR.
@param output_file is the output file to store the result of the query. *)
@param prover is the {!Prover.t} for the verification query.
@param prover_altern
is an optional alternative [prover] configuration, as specified in the
file [caisar_detection.conf].
@param problem is a {!Problem.t} value. *)
val of_json : string -> t
val pretty : Format.formatter -> t -> unit
val of_json :
?memlimit:string -> ?timelimit:string -> ?outfile:string -> string -> t
(** Create a query from a JSON file.
@param memlimit is the memory limit granted to the verification.
@param timelimit is the timeout granted to the verification.
@param outfile is the output file to store the result of the query. *)
val memlimit_of_string : string -> int (* TO BE REMOVED *)
val timelimit_of_string : string -> int (* TO BE REMOVED *)
end
(** The answer of a verification query by CAISAR. *)
module Answer : sig
(** The answer of a verification query by CAISAR. *)
type t = private {
id : int;
problem_answer : problem_answer;
......@@ -147,7 +147,7 @@ module Answer : sig
id : Why3.Decl.prsymbol;
prover_answer : prover_answer;
additional_info : string option;
(* Additional information provided by the prover *)
(** Additional information provided by the prover. *)
}
[@@deriving to_yojson, show]
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment