From f054eea1063124c252ad88ab23f2e468aa72bed8 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 14 Feb 2023 12:19:57 +0100
Subject: [PATCH] [verification] Rework additional information for dataset
results and simplify its JSON serialization.
---
src/JSON.ml | 2 +-
src/JSON.mli | 2 +-
src/main.ml | 52 ++++++++++++++++++--------------------------
src/verification.ml | 43 +++++++++++-------------------------
src/verification.mli | 9 ++++----
5 files changed, 41 insertions(+), 67 deletions(-)
diff --git a/src/JSON.ml b/src/JSON.ml
index 502f4be..9ed36e5 100644
--- a/src/JSON.ml
+++ b/src/JSON.ml
@@ -43,7 +43,7 @@ type output = {
id : string;
prover_answer : prover_answer;
percentage_valid : float;
- dataset_results : string;
+ dataset_results : prover_answer list;
}
and prover_answer = Call_provers.prover_answer =
diff --git a/src/JSON.mli b/src/JSON.mli
index 96a7b6c..550cb40 100644
--- a/src/JSON.mli
+++ b/src/JSON.mli
@@ -42,7 +42,7 @@ type output = {
id : string;
prover_answer : prover_answer;
percentage_valid : float;
- dataset_results : string;
+ dataset_results : prover_answer list;
}
and prover_answer = Call_provers.prover_answer =
diff --git a/src/main.ml b/src/main.ml
index d7d68f1..00b42e0 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -149,40 +149,30 @@ let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
List.iter theory_answers ~f:log_theory_answer;
theory_answers
-let record_dataset_results id prover_answer dataset outfile =
+let record_json_output id prover_answer dataset_results file =
let percentage_valid =
let nb_valid =
- List.count dataset ~f:(fun record ->
- match List.hd_exn record with "Valid" -> true | _ -> false)
+ List.count dataset_results ~f:(fun prover_answer ->
+ match prover_answer with Why3.Call_provers.Valid -> true | _ -> false)
in
let nb_valid = Float.of_int nb_valid in
- let total = Float.of_int (List.length dataset) in
+ let total = Float.of_int (List.length dataset_results) in
nb_valid /. total *. 100.
in
- let dataset_results =
- let dataset_results, csv_out_channel =
- let filename, out_channel =
- Caml.Filename.open_temp_file "caisar" "results.csv"
- in
- (filename, Csv.to_channel out_channel)
- in
- Csv.output_all csv_out_channel dataset;
- Csv.close_out csv_out_channel;
- dataset_results
- in
let output = { JSON.id; prover_answer; percentage_valid; dataset_results } in
- let out_channel = Stdlib.open_out outfile in
+ let out_channel = Stdlib.open_out file in
Yojson.Safe.to_channel out_channel (JSON.output_to_yojson output);
- Logs.info (fun m -> m "@[Results recorded in file '%s'@]" outfile);
+ Logs.info (fun m -> m "@[Results recorded in file '%s'@]" file);
Stdlib.close_out out_channel
-let record_theory_answers id outfile =
- Why3.Wstdlib.Mstr.iter (fun theory_name task_answers ->
- match task_answers with
- | [ { Verification.prover_answer; additional_info = Dataset dataset; _ } ]
- ->
- record_dataset_results id prover_answer dataset outfile
- | _ -> failwith (Fmt.str "Unexpected answers for theory '%s'" theory_name))
+let record_verification_result id verification_result file =
+ Why3.Wstdlib.Mstr.iter
+ (fun name (answers : Verification.answer list) ->
+ match answers with
+ | [ { prover_answer; additional_info = Dataset dataset_results; _ } ] ->
+ record_json_output id prover_answer dataset_results file
+ | _ -> failwith (Fmt.str "Unexpected answers for theory '%s'" name))
+ verification_result
let verify_json ?memlimit ?timelimit ?outfile json =
let jin = JSON.input_of_string json in
@@ -202,16 +192,16 @@ let verify_json ?memlimit ?timelimit ?outfile json =
(* Precedence to the command line option, if any. *)
match outfile with Some _ -> outfile | None -> jin.output_file
in
- let file = Result.ok_or_failwith (Verification.File.of_json_input jin) in
- let theory_answers =
+ let infile = Result.ok_or_failwith (Verification.File.of_json_input jin) in
+ let verification_results =
verify ~loadpath:[] ?memlimit ?timelimit ~dataset:jin.property.dataset
- jin.prover [ file ]
+ jin.prover [ infile ]
in
- match theory_answers with
+ match verification_results with
| [] -> assert false (* We always build one theory from the provided JSON. *)
- | [ theory_answer ] ->
- Option.iter outfile ~f:(fun outfile ->
- record_theory_answers jin.id outfile theory_answer)
+ | [ verification_result ] ->
+ Option.iter outfile
+ ~f:(record_verification_result jin.id verification_result)
| _ -> failwith "Unexpected more than one theory from a JSON file"
let exec_cmd cmdname cmd =
diff --git a/src/verification.ml b/src/verification.ml
index b606275..1f9a37d 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -57,7 +57,7 @@ module File = struct
| JSON jin -> JSON.pretty_input fmt jin
end
-type theory_answer = answer list Wstdlib.Mstr.t
+type verification_result = answer list Wstdlib.Mstr.t
and answer = {
id : Decl.prsymbol;
@@ -67,7 +67,7 @@ and answer = {
and additional_info =
| Generic of string option
- | Dataset of Csv.t
+ | Dataset of Call_provers.prover_answer list
let () =
Language.register_nnet_support ();
@@ -116,12 +116,12 @@ let answer_saver limit config env config_prover dataset task =
match answer.prover_answer with
| Call_provers.Unknown "" ->
let additional_info = Fmt.str "%d/%d" answer.nb_proved answer.nb_total in
- (Call_provers.Unknown additional_info, None)
+ (Call_provers.Unknown additional_info, Generic None)
| Call_provers.Unknown _ ->
assert false (* By construction of SAVer's Unknown answer. *)
| prover_answer ->
let additional_info = Fmt.str "(%d/%d)" answer.nb_proved answer.nb_total in
- (prover_answer, Some additional_info)
+ (prover_answer, Generic (Some additional_info))
let answer_aimos limit config env config_prover dataset task aimos_config =
let predicate =
@@ -156,7 +156,7 @@ let answer_aimos limit config env config_prover dataset task aimos_config =
let answer =
AIMOS.call_prover limit config config_prover predicate aimos_filename
in
- let additional_info = None in
+ let additional_info = Generic None in
(answer, additional_info)
let nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
@@ -230,12 +230,7 @@ let answer_dataset limit config env prover config_prover driver dataset task =
Csv.close_in csv_in_channel;
if List.length dataset <> List.length dataset_answers
then failwith "Inconsistent number of prover answers and dataset records"
- else
- List.map2_exn dataset dataset_answers ~f:(fun record prover_answer ->
- let result =
- Fmt.str "%a" Call_provers.print_prover_answer prover_answer
- in
- result :: record)
+ else Dataset dataset_answers
in
(prover_answer, additional_info)
@@ -261,33 +256,21 @@ let answer_generic limit config env prover config_prover driver task =
List.map tasks ~f:(call_prover_on_task limit config command driver)
in
let prover_answer = combine_prover_answers answers in
- (prover_answer, None)
+ let additional_info = Generic None in
+ (prover_answer, additional_info)
let call_prover ?dataset ~limit config env prover config_prover driver task =
let prover_answer, additional_info =
match prover with
- | Prover.Saver ->
- let prover_answer, additional_info =
- answer_saver limit config env config_prover dataset task
- in
- (prover_answer, Generic additional_info)
+ | Prover.Saver -> answer_saver limit config env config_prover dataset task
| Aimos ->
- let prover_answer, additional_info =
- (* TODO: add real config file *)
- answer_aimos limit config env config_prover dataset task None
- in
- (prover_answer, Generic additional_info)
+ (* TODO: add real config file *)
+ answer_aimos limit config env config_prover dataset task None
| (Marabou | Pyrat | Nnenum) when Option.is_some dataset ->
let dataset = Unix.realpath (Option.value_exn dataset) in
- let prover_answer, additional_info =
- answer_dataset limit config env prover config_prover driver dataset task
- in
- (prover_answer, Dataset additional_info)
+ answer_dataset limit config env prover config_prover driver dataset task
| Marabou | Pyrat | CVC5 | Nnenum ->
- let prover_answer, additional_info =
- answer_generic limit config env prover config_prover driver task
- in
- (prover_answer, Generic additional_info)
+ answer_generic limit config env prover config_prover driver task
in
let id = Task.task_goal task in
{ id; prover_answer; additional_info }
diff --git a/src/verification.mli b/src/verification.mli
index 1c93426..8dc3939 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -30,7 +30,7 @@ module File : sig
val pretty : Format.formatter -> t -> unit
end
-type theory_answer = answer list Wstdlib.Mstr.t
+type verification_result = answer list Wstdlib.Mstr.t
and answer = private {
id : Decl.prsymbol;
@@ -40,7 +40,8 @@ and answer = private {
and additional_info = private
| Generic of string option
- | Dataset of Csv.t
+ | Dataset of Call_provers.prover_answer list
+ (** A prover answer per data point. *)
val verify :
?debug:bool ->
@@ -52,8 +53,8 @@ val verify :
Prover.t ->
?prover_altern:string ->
File.t ->
- theory_answer
-(** [verify debug format loadpath memlimit timelimit dataset prover prover_altern file]
+ verification_result
+(** [verify ?debug ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern file]
launches a verification of the given [file] with the provided [prover] and
[dataset].
--
GitLab