Newer
Older
(**************************************************************************)
(* *)
(* This file is part of CAISAR. *)
(* *)
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
(* You can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
(* Foundation, version 2.1. *)
(* *)
(* It is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU Lesser General Public License for more details. *)
(* *)
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
open Why3
open Base
module File = struct
type t =
| Stdin
| File of string
[@@deriving of_yojson, show]
let of_string s =
if String.equal s "-"
then Ok Stdin
else if Stdlib.Sys.file_exists 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
end
module Problem = struct
type t =
| GenericProblem of {
filepath : File.t;
theories : string list;
}
[@@deriving of_yojson { strict = false }, show]
let of_file ?(definitions = []) ?(theories = []) ?(goals = []) file =
(* TODO: analyze the property inside of the filepath in order to extract the
proper dataset predicate? *)
GenericProblem { filepath = file; definitions; theories; goals }
end
module Query = struct
let id_int = ref 0
type t = {
id : string;
prover : Prover.t;
prover_altern : string option;
problem : Problem.t;
loadpath : string list;
time_limit : int option;
memory_limit : int option;
onnx_out_dir : string option;
output_file : string option;
dataset : string option;
}
[@@deriving of_yojson { strict = false }, show]
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
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 =
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;
prover_altern;
loadpath;
time_limit;
problem;
memory_limit;
onnx_out_dir;
dataset;
}
let of_json ?memlimit ?timelimit ?outfile s =
let query =
match of_yojson (Yojson.Safe.from_file s) with
| Ok t -> t
| Error msg ->
Logging.user_error (fun m ->
m "Unrecognized JSON configuration in file '%s' (%s)" s msg)
Logging.user_error (fun m ->
m "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 specified while creating verification query from \
JSON file@]"))
| Some _ as output_file -> { query with output_file }
let pretty fmt = Fmt.fmt "%a" fmt pp
end
module Answer = struct
let prsymbol_to_yojson pr = `String (Fmt.str "%a" Pretty.print_pr pr)
let pp_prsymbol fmt pr = Fmt.pf fmt "%a" Pretty.print_pr pr
type t = {
problem_answer : problem_answer;
}
[@@deriving to_yojson, show]
and prover_answer = Call_provers.prover_answer =
| Valid
| Invalid
| Timeout
| OutOfMemory
| StepLimitExceeded
| Unknown of string
| Failure of string
| HighFailure
[@@deriving to_yojson, show]
and problem_answer =
| LegacyDatasetAnswer of {
id : Why3.Decl.prsymbol;
[@to_yojson prsymbol_to_yojson] [@printer pp_prsymbol]
prover_answer : prover_answer;
percentage_valid : float option;
dataset_results : prover_answer list;
additional_info : string option;
}
| GenericProblemAnswer of {
id : Why3.Decl.prsymbol;
[@to_yojson prsymbol_to_yojson] [@printer pp_prsymbol]
prover_answer : prover_answer;
additional_info : string option;
}
[@@deriving to_yojson, show]
let make ~(query : Query.t) problem_answer =
let id = "answer" in
let id =
Int.incr id_int;
let query_id = query.id in
{ id; query_id; problem_answer }
let pretty fmt = Fmt.fmt "%a" fmt pp
end