verification_types.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(*  Copyright (C) 2024                                                    *)
(*    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;
        definitions : (string * string) list;
        theories : string list;
        goals : (string * string list) 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]

  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 = "caisar_verification_query" in
    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;
      output_file = None;
      dataset;
    }

  let of_json ?memlimit ?timelimit ?outfile s =
    let query =
      match of_yojson (Yojson.Safe.from_file s) with
      | Ok t -> t
      | Error msg ->
        invalid_arg
          (Fmt.str "Unrecognized JSON configuration in file '%s' (%s)" s msg)
      | exception Yojson.Json_error msg ->
        failwith
          (Fmt.str "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 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
  let id = ref 0

  type t = {
    id : int;
    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 p =
    Int.incr id;
    { id = !id; problem_answer = p }

  let pretty fmt = Fmt.fmt "%a" fmt pp
end