[verification] Introduce verification result type.

Decouple the verification process from its result logging.

src/main.ml

@@ -119,16 +119,34 @@ let timelimit_of_string s =
   | [ v ], [ "h" ] -> Int.of_string v * 3600
   | _ -> invalid_arg "Unrecognized time limit"
 
-let verify ?format ~loadpath ?memlimit ?timelimit ?dataset ?outfile prover files
-    =
+let log_theory_answer =
+  let open Why3 in
+  Wstdlib.Mstr.iter (fun theory_name task_answers ->
+    Logs.info (fun m ->
+      m "@[Verification results for theory `%s'@]" theory_name);
+    List.iter task_answers
+      ~f:(fun { Verification.id; result; additional_info } ->
+      let additional_info =
+        match additional_info with Generic s -> s | Dataset _ -> None
+      in
+      Logs.app (fun m ->
+        m "@[Goal %a:@ %a%a@]" Pretty.print_pr id
+          Call_provers.print_prover_answer result
+          Fmt.(option ~none:nop (any " " ++ string))
+          additional_info)))
+
+let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover 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
-         ?dataset ?outfile prover)
-    files
+  let theory_answers =
+    List.map files
+      ~f:
+        (Verification.verify ~debug ?format ~loadpath ?memlimit ?timelimit
+           ?dataset prover)
+  in
+  List.iter theory_answers ~f:log_theory_answer;
+  theory_answers
 
 let verify_json ?memlimit ?timelimit ?outfile json =
   let jin = Result.ok_exn (Verification.JSON.input_of_string json) in
@@ -147,11 +165,11 @@ let verify_json ?memlimit ?timelimit ?outfile json =
     | None -> Option.map jin.time_limit ~f:Int.to_string
     | Some _ -> timelimit
   in
-  let outfile =
+  let _outfile =
     (* Precedence to the command line option, if any. *)
     match outfile with None -> jin.output_file | Some _ -> outfile
   in
-  verify ~loadpath:[] ?memlimit ?timelimit ~dataset ?outfile prover [ file ]
+  verify ~loadpath:[] ?memlimit ?timelimit ~dataset prover [ file ]
 
 let exec_cmd cmdname cmd =
   Logs.debug (fun m -> m "Command `%s'" cmdname);
@@ -251,7 +269,8 @@ let verify_cmd =
     Term.(
       const (fun format loadpath memlimit timelimit prover dataset files _ ->
         exec_cmd cmdname (fun () ->
-          verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover files))
+          ignore
+            (verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover files)))
       $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset $ files
       $ setup_logs)
   in

src/verification.ml

@@ -187,6 +187,18 @@ module File = struct
     | Json j -> JSON.pretty fmt j
 end
 
+type theory_answer = answer list Wstdlib.Mstr.t
+
+and answer = {
+  id : Decl.prsymbol;
+  result : Call_provers.prover_answer;
+  additional_info : additional_info;
+}
+
+and additional_info =
+  | Generic of string option
+  | Dataset of Csv.t
+
 let () =
   Language.register_nnet_support ();
   Language.register_onnx_support ();
@@ -253,45 +265,44 @@ let combine_prover_answers answers =
     | Call_provers.Valid, r | r, Call_provers.Valid -> r
     | _ -> acc)
 
-let record_dataset_results ~dataset ~dataset_answers prover_answer outfile =
-  let percentage_valid =
-    let count =
-      List.count dataset_answers ~f:(fun prover_answer ->
-        match prover_answer with Call_provers.Valid -> true | _ -> false)
-    in
-    Float.of_int count /. Float.of_int (List.length dataset_answers) *. 100.
-  in
-  let dataset_results =
-    let csv_in_channel = Csv.of_channel (Stdlib.open_in dataset) in
-    let dataset_results, csv_out_channel =
-      let filename, out_channel =
-        Filename.open_temp_file "caisar" "results.csv"
-      in
-      (filename, Csv.to_channel out_channel)
-    in
-    let dataset = Csv.input_all csv_in_channel in
-    Csv.close_in csv_in_channel;
-    if List.length dataset = List.length dataset_answers
-    then
-      List.iter2_exn dataset dataset_answers ~f:(fun record prover_answer ->
-        let result =
-          Fmt.str "%a" Call_provers.print_prover_answer prover_answer
-        in
-        let record = result :: record in
-        Csv.output_record csv_out_channel record);
-    Csv.close_out csv_out_channel;
-    dataset_results
-  in
-  let output =
-    { JSON.result = prover_answer; percentage_valid; dataset_results }
-  in
-  let out_channel = Stdlib.open_out outfile in
-  Yojson.Safe.to_channel out_channel (JSON.output_to_yojson output);
-  Logs.info (fun m -> m "@[Results recorded in file '%s'@]" outfile);
-  Stdlib.close_out out_channel
+(* let record_dataset_results ~dataset ~dataset_answers prover_answer outfile =
+ *   let percentage_valid =
+ *     let count =
+ *       List.count dataset_answers ~f:(fun prover_answer ->
+ *         match prover_answer with Call_provers.Valid -> true | _ -> false)
+ *     in
+ *     Float.of_int count /. Float.of_int (List.length dataset_answers) *. 100.
+ *   in
+ *   let dataset_results =
+ *     let csv_in_channel = Csv.of_channel (Stdlib.open_in dataset) in
+ *     let dataset_results, csv_out_channel =
+ *       let filename, out_channel =
+ *         Filename.open_temp_file "caisar" "results.csv"
+ *       in
+ *       (filename, Csv.to_channel out_channel)
+ *     in
+ *     let dataset = Csv.input_all csv_in_channel in
+ *     Csv.close_in csv_in_channel;
+ *     if List.length dataset = List.length dataset_answers
+ *     then
+ *       List.iter2_exn dataset dataset_answers ~f:(fun record prover_answer ->
+ *         let result =
+ *           Fmt.str "%a" Call_provers.print_prover_answer prover_answer
+ *         in
+ *         let record = result :: record in
+ *         Csv.output_record csv_out_channel record);
+ *     Csv.close_out csv_out_channel;
+ *     dataset_results
+ *   in
+ *   let output =
+ *     { JSON.result = prover_answer; percentage_valid; dataset_results }
+ *   in
+ *   let out_channel = Stdlib.open_out outfile in
+ *   Yojson.Safe.to_channel out_channel (JSON.output_to_yojson output);
+ *   Logs.info (fun m -> m "@[Results recorded in file '%s'@]" outfile);
+ *   Stdlib.close_out out_channel *)
 
-let answer_dataset ?outfile limit config env prover config_prover driver dataset
-  task =
+let answer_dataset limit config env prover config_prover driver dataset task =
   let dataset_predicate =
     let on_model ls =
       let message =
@@ -316,31 +327,42 @@ let answer_dataset ?outfile limit config env prover config_prover driver dataset
     Dataset.tasks_of_nn_csv_predicate env dataset_predicate
     |> List.map ~f:(Driver.prepare_task driver)
   in
-  let tasks =
-    (* We turn each task in [dataset_tasks] into a list (ie, conjunction) of
-       disjunctions of tasks. *)
-    match prover with
-    | Prover.Marabou -> List.map ~f:(Trans.apply Split.split_all) dataset_tasks
-    | _ -> [ dataset_tasks ]
-  in
   let command = Whyconf.get_complete_command ~with_steps:false config_prover in
   let command =
     let nn_file = Unix.realpath dataset_predicate.model.filename in
     Re__Core.replace_string nnet_or_onnx ~by:nn_file command
   in
   let dataset_answers =
-    List.map tasks ~f:(fun dataset_elt_tasks ->
-      let dataset_elt_answers =
-        List.map dataset_elt_tasks
-          ~f:(call_prover_on_task limit config command driver)
-      in
-      combine_prover_answers dataset_elt_answers)
+    match prover with
+    | Prover.Marabou ->
+      (* We turn each task in [dataset_tasks] into a list (ie, conjunction) of
+         disjunctions of tasks. *)
+      let tasks = List.map ~f:(Trans.apply Split.split_all) dataset_tasks in
+      List.map tasks ~f:(fun dataset_elt_tasks ->
+        let dataset_elt_answers =
+          List.map dataset_elt_tasks
+            ~f:(call_prover_on_task limit config command driver)
+        in
+        combine_prover_answers dataset_elt_answers)
+    | _ ->
+      List.map dataset_tasks
+        ~f:(call_prover_on_task limit config command driver)
   in
   let prover_answer = combine_prover_answers dataset_answers in
-  Option.iter
-    ~f:(record_dataset_results ~dataset ~dataset_answers prover_answer)
-    outfile;
-  (prover_answer, None)
+  let additional_info =
+    let csv_in_channel = Csv.of_channel (Stdlib.open_in dataset) in
+    let dataset = Csv.input_all csv_in_channel in
+    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)
+  in
+  (prover_answer, additional_info)
 
 let answer_generic limit config env prover config_prover driver task =
   let task = Proof_strategy.apply_native_nn_prover env task in
@@ -366,26 +388,31 @@ let answer_generic limit config env prover config_prover driver task =
   let prover_answer = combine_prover_answers answers in
   (prover_answer, None)
 
-let call_prover ?dataset ?outfile ~limit config env prover config_prover driver
-  task =
-  let prover_answer, additional_info =
+let call_prover ?dataset ~limit config env prover config_prover driver task =
+  let result, additional_info =
     match prover with
-    | Prover.Saver -> answer_saver limit config env config_prover dataset task
+    | Prover.Saver ->
+      let prover_answer, additional_info =
+        answer_saver limit config env config_prover dataset task
+      in
+      (prover_answer, Generic additional_info)
     | (Marabou | Pyrat | Nnenum) when Option.is_some dataset ->
       let dataset = Unix.realpath (Option.value_exn dataset) in
-      answer_dataset ?outfile limit config env prover config_prover driver
-        dataset task
+      let prover_answer, additional_info =
+        answer_dataset limit config env prover config_prover driver dataset task
+      in
+      (prover_answer, Dataset additional_info)
     | Marabou | Pyrat | CVC5 | Nnenum ->
-      answer_generic limit config env prover config_prover driver task
+      let prover_answer, additional_info =
+        answer_generic limit config env prover config_prover driver task
+      in
+      (prover_answer, Generic additional_info)
   in
-  Logs.app (fun m ->
-    m "@[Goal %a:@ %a%a@]" Pretty.print_pr (Task.task_goal task)
-      Call_provers.print_prover_answer prover_answer
-      Fmt.(option ~none:nop (any " " ++ string))
-      additional_info)
+  let id = Task.task_goal task in
+  { id; result; additional_info }
 
 let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
-  ?outfile prover file =
+  prover file =
   if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
   let env, config = create_env ~debug loadpath in
   let main = Whyconf.get_main config in
@@ -408,8 +435,8 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
       mlw_files
     | Json json -> JSON.mstr_theory_of_json env json
   in
-  Wstdlib.Mstr.iter
-    (fun _ theory ->
+  Wstdlib.Mstr.map
+    (fun theory ->
       let tasks = Task.split_theory theory None None in
       let config_prover =
         let altern =
@@ -433,9 +460,7 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
           in
           Driver.load_driver_absolute env file config_prover.extra_drivers
       in
-      List.iter
-        ~f:
-          (call_prover ?dataset ?outfile ~limit main env prover config_prover
-             driver)
+      List.map
+        ~f:(call_prover ?dataset ~limit main env prover config_prover driver)
         tasks)
     mstr_theory

src/verification.mli

@@ -20,6 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Why3
+
 module JSON : sig
   type input = private {
     prover : Prover.t;
@@ -35,7 +37,7 @@ module JSON : sig
     normalization : Dataset.normalization option;
     kind : Dataset.property;
   }
-  [@@deriving yojson, show]
+  [@@deriving yojson { strict = false }, show]
 
   type output = private {
     result : prover_answer;
@@ -43,7 +45,7 @@ module JSON : sig
     dataset_results : string;
   }
 
-  and prover_answer = Why3.Call_provers.prover_answer =
+  and prover_answer = Call_provers.prover_answer =
     | Valid
     | Invalid
     | Timeout
@@ -66,6 +68,18 @@ module File : sig
   val pretty : Format.formatter -> t -> unit
 end
 
+type theory_answer = answer list Wstdlib.Mstr.t
+
+and answer = private {
+  id : Decl.prsymbol;
+  result : Call_provers.prover_answer;
+  additional_info : additional_info;
+}
+
+and additional_info = private
+  | Generic of string option
+  | Dataset of Csv.t
+
 val verify :
   ?debug:bool ->
   ?format:string ->
@@ -73,13 +87,11 @@ val verify :
   ?memlimit:int ->
   ?timelimit:int ->
   ?dataset:string ->
-  ?outfile:string ->
   Prover.t ->
   File.t ->
-  unit
-(** [verify debug format loadpath memlimit timeout dataset outfile prover file]
-    launches a verification of the given [file] with the provided [prover] and
-    [dataset].
+  theory_answer
+(** [verify debug format loadpath memlimit timeout dataset prover file] launches
+    a verification of the given [file] with the provided [prover] and [dataset].
 
     @param debug when set, enables debug information.
     @param format is the [file] format.
@@ -90,4 +102,6 @@ val verify :
     @param dataset
       is the filepath of a dataset (eg, in CSV format) possibly appearing in
       [file].
-    @param outfile is the filepath where recording the verification results. *)
+    @return
+      for each theory, an [answer] for each goal of the theory, respecting the
+      order of appearance. *)