saver.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(*  Copyright (C) 2023                                                    *)
(*    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

let re_svm = Re__Core.(compile (str "%{svm}"))
let re_dataset = Re__Core.(compile (str "%{dataset}"))
let re_eps = Re__Core.(compile (str "%{epsilon}"))
let re_abstraction = Re__Core.(compile (str "%{abstraction}"))
let re_distance = Re__Core.(compile (str "%{distance}"))

let build_command config_prover svm_filename dataset_filename eps =
  let command = Whyconf.get_complete_command ~with_steps:false config_prover in
  let params =
    [
      (re_svm, Unix.realpath svm_filename);
      (re_dataset, Unix.realpath dataset_filename);
      (re_eps, Option.(value (map ~f:Dataset.string_of_eps eps)) ~default:"0");
      (re_distance, "l_inf");
      (re_abstraction, "hybrid");
    ]
  in
  List.fold params ~init:command ~f:(fun cmd (param, by) ->
    Re__Core.replace_string param ~by cmd)

type answer = {
  prover_answer : Call_provers.prover_answer;
  nb_total : int;
  nb_proved : int;
}

(* SAVer output is made of 7 columns separated by (multiple) space(s) of the
   following form:

   [SUMMARY] integer float float integer integer integer

   We are interested in recovering the integers. The following regexp matches
   groups of one or more digits by means of '(\\d+)'. The latter is used 4 times
   for the 4 columns of integers we are interested in. The 1st group reports the
   number of total data points in the dataset, 2nd group reports the number of
   correct data points, 3rd group reports the number of robust data points, 4th
   group reports the number of conditionally robust (ie, correct and robust)
   data points. *)
let re_saver_output =
  Re__Pcre.regexp
    "\\[SUMMARY\\]\\s*(\\d+)\\s*[0-9.]+\\s*[0-9.]+\\s*(\\d)+\\s*(\\d+)\\s*(\\d+)"

(* The dataset size is the first group of digits matched by
   [re_saver_output]. *)
let re_group_number_dataset_size = 1

(* Regexp group number as matched by [re_saver_output] for each predicate. *)
let re_group_number_of_predicate = function
  | Dataset.Correct -> 2
  | Robust _ -> 3
  | CondRobust _ -> 4
  | MetaRobust _ -> failwith "Unsupported metamorphic robustness predicate"

let negative_answer = function
  | Dataset.Correct ->
    (* SAVer is complete wrt [Correct] predicate. *)
    Call_provers.Invalid
  | Robust _ | CondRobust _ -> Call_provers.Unknown ""
  | MetaRobust _ -> failwith "Unsupported metamorphic robustness predicate"

let build_answer predicate_kind prover_result =
  match prover_result.Call_provers.pr_answer with
  | Call_provers.HighFailure -> (
    let pr_output = prover_result.pr_output in
    match Re__Core.exec_opt re_saver_output pr_output with
    | Some re_group ->
      let nb_total =
        Int.of_string (Re__Core.Group.get re_group re_group_number_dataset_size)
      in
      let nb_proved =
        let re_group_number = re_group_number_of_predicate predicate_kind in
        Int.of_string (Re__Core.Group.get re_group re_group_number)
      in
      let prover_answer =
        if nb_total = nb_proved
        then Call_provers.Valid
        else negative_answer predicate_kind
      in
      { prover_answer; nb_total; nb_proved }
    | None -> failwith "Cannot interpret the output provided by SAVer")
  | _ ->
    (* Any other answer than HighFailure should never happen as we do not define
       anything in SAVer's driver. *)
    assert false

let call_prover limit config config_prover predicate =
  let command =
    let svm = predicate.Dataset.model.Language.filename in
    let dataset = predicate.dataset in
    let eps =
      match predicate.property with
      | Dataset.Correct -> None
      | Robust e | CondRobust e -> Some e
      | MetaRobust _ -> failwith "Unsupported metamorphic robustness predicate"
    in
    build_command config_prover svm dataset eps
  in
  let prover_call =
    let res_parser =
      {
        Call_provers.prp_regexps =
          [ ("NeverMatch", Call_provers.Failure "Should not happen in CAISAR") ];
        prp_timeregexps = [];
        prp_stepregexps = [];
        prp_exitcodes = [];
        prp_model_parser = Model_parser.lookup_model_parser "no_model";
      }
    in
    Call_provers.call_on_buffer ~command ~config ~limit ~res_parser
      ~filename:" " ~get_model:None ~gen_new_file:false (Buffer.create 10)
  in
  let prover_result = Call_provers.wait_on_call prover_call in
  build_answer predicate.property prover_result