verification.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(**************************************************************************)

open Why3
open Base
module Filename = Caml.Filename

let () =
  Language.register_nnet_support ();
  Language.register_onnx_support ()

let create_env loadpath =
  let config = Autodetect.autodetection ~debug:true () in
  let config =
    let main = Whyconf.get_main config in
    let dft_memlimit = 4000 (* 4 GB *) in
    let main =
      Whyconf.(
        set_limits main (timelimit main) dft_memlimit (running_provers_max main))
    in
    Whyconf.set_main config main
  in
  let stdlib = Dirs.Sites.stdlib in
  ( Env.create_env
      (loadpath @ stdlib @ Whyconf.loadpath (Whyconf.get_main config)),
    config )

let nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))

let combine_prover_answers answers =
  List.fold_left answers ~init:Call_provers.Valid ~f:(fun acc r ->
    match (acc, r) with
    | Call_provers.Valid, r | r, Call_provers.Valid -> r
    | _ -> acc)

let call_prover ~limit config (prover : Whyconf.config_prover) driver task =
  let task_prepared = Driver.prepare_task driver task in
  let tasks =
    (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
    if String.equal prover.prover.prover_name "Marabou"
    then Trans.apply Split_goal.split_goal_full task_prepared
    else [ task_prepared ]
  in
  let command = Whyconf.get_complete_command ~with_steps:false prover in
  let nn_file =
    match Task.on_meta_excl Native_nn_prover.meta_nn_filename task_prepared with
    | Some [ MAstr nn_file ] -> nn_file
    | Some _ -> assert false (* By construction of the meta. *)
    | None -> invalid_arg (Fmt.str "No neural network model found in task")
  in
  let nn_file = Unix.realpath nn_file in
  let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
  let call_prover_on_task task_prepared =
    let prover_call =
      Driver.prove_task_prepared ~libdir:(Whyconf.libdir config)
        ~datadir:(Whyconf.datadir config) ~command ~limit driver task_prepared
    in
    let prover_result = Call_provers.wait_on_call prover_call in
    prover_result.pr_answer
  in
  let answers = List.map tasks ~f:call_prover_on_task in
  let answer = combine_prover_answers answers in
  Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
    Call_provers.print_prover_answer answer

let verify ?(debug = false) format loadpath ?memlimit ?timeout prover file =
  if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
  let env, config = create_env loadpath in
  let steplimit = None in
  let steps = match steplimit with Some 0 -> None | _ -> steplimit in
  let limit =
    let memlimit =
      Option.value memlimit ~default:Whyconf.(memlimit (get_main config))
    in
    let def = Call_provers.empty_limit in
    {
      Call_provers.limit_time = Opt.get_def def.limit_time timeout;
      Call_provers.limit_steps = Opt.get_def def.limit_time steps;
      Call_provers.limit_mem = memlimit;
    }
  in
  let _, mstr_theory =
    match file with
    | "-" ->
      ("stdin", Env.(read_channel ?format base_language env "stdin" Caml.stdin))
    | file ->
      let mlw_files, _ = Env.(read_file ?format base_language env file) in
      (file, mlw_files)
  in
  Wstdlib.Mstr.iter
    (fun _ theory ->
      let tasks = Task.split_theory theory None None in
      let prover =
        let prover = Prover.to_string prover in
        Whyconf.(filter_one_prover config (mk_filter_prover prover))
      in
      let driver =
        match String.chop_prefix ~prefix:"caisar_drivers/" prover.driver with
        | None -> Whyconf.(load_driver (get_main config) env prover)
        | Some file ->
          let file =
            Filename.concat
              (Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
              file
          in
          Driver.load_driver_absolute env file prover.extra_drivers
      in
      List.iter
        ~f:(call_prover ~limit (Whyconf.get_main config) prover driver)
        tasks)
    mstr_theory