aimos.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_aimos_file = Re__Core.(compile (str "%{aimos_file}"))

let write_config inputs_path models_path perturbation perturbation_path out_mode
  amplitude =
  let config_file = Stdlib.Filename.temp_file "aimos-" ".yml" in
  let config_path = Fpath.v config_file in
  let cwd = Stdlib.Sys.getcwd () in
  let ampli = Dataset.string_of_amplitude amplitude in
  let transformations =
    match ampli with
    | None -> `A [ `O [ ("name", `String perturbation) ] ]
    | Some a ->
      `A [ `O [ ("name", `String perturbation); ("fn_range", `String a) ] ]
  in
  let options =
    match perturbation_path with
    | "" ->
      `O
        [
          ("plot", `Bool false);
          ("inputs_path", `String inputs_path);
          ("transformations", transformations);
          ("alt_cwd", `String cwd);
        ]
    | ctp ->
      `O
        [
          ("plot", `Bool false);
          ("inputs_path", `String inputs_path);
          ("transformations", transformations);
          ("custom_t_path", `String ctp);
          ("alt_cwd", `String cwd);
        ]
  in
  let models =
    match out_mode with
    | "" ->
      `A [ `O [ ("defaults", `O [ ("models_path", `String models_path) ]) ] ]
    | om ->
      `A
        [
          `O
            [
              ( "defaults",
                `O
                  [
                    ("models_path", `String models_path);
                    ("out_mode", `String om);
                  ] );
            ];
        ]
  in
  let full_config = `O [ ("options", options); ("models", models) ] in
  Yaml_unix.to_file_exn config_path full_config;
  config_file

let build_command config_prover
  (predicate : (Language.nn_shape, string) Dataset.predicate) =
  let inputs_path = Unix.realpath predicate.dataset in
  let models_path = Unix.realpath predicate.model.filename in
  let perturbation, amplitude, perturbation_path, out_mode =
    match predicate.property with
    | Dataset.MetaRobust (_, aimos_params) ->
      ( aimos_params.perturbation,
        aimos_params.amplitude,
        aimos_params.ctp,
        aimos_params.om )
    | _ -> failwith "Unsupported property"
  in
  let aimos_config =
    write_config inputs_path models_path perturbation perturbation_path out_mode
      amplitude
  in
  let command = Whyconf.get_complete_command ~with_steps:false config_prover in
  Re__Core.replace_string re_aimos_file ~by:aimos_config command

let re_aimos_output = Re__Pcre.regexp "((,\\s)(\\d+\\.\\d+))"

let build_answer predicate_kind prover_result =
  let threshold =
    match predicate_kind with
    | Dataset.MetaRobust (f, _) ->
      Float.of_string (Dataset.string_of_threshold f)
    | _ -> failwith "Unsupported property"
  in
  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_aimos_output pr_output with
    | Some re_group ->
      (* The regex matches the only group (the 3rd one) that contains
         dot-separated numerical values that follow a comma and a space. This is
         not ideal as there might be edge cases where the regex matches other
         parts of the output that are not supposed to be matched. This will be
         fixed later on, but for now is good enough. *)
      let res_aimos = Float.of_string (Re__Core.Group.get re_group 3) in
      let prover_answer =
        if Float.( >= ) res_aimos threshold
        then Call_provers.Valid
        else Call_provers.Invalid
      in
      prover_answer
    | None -> failwith "Cannot interpret the output provided by AIMOS")
  | _ ->
    (* Any other answer than HighFailure should never happen as we do not define
       anything in AIMOS's driver. *)
    assert false

let call_prover limit config config_prover
  (predicate : (Language.nn_shape, string) Dataset.predicate) =
  let command = build_command config_prover predicate 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