verification.ml

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

open Base
module Filename = Caml.Filename

let () = Language.register_nnet_support ()

let create_env loadpath =
  let config = Autodetection.autodetect ~debug:true () in
  let open Why3 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.compile (Re.str "%{nnet-onnx}")

let call_prover ~limit prover driver task =
  let open Why3 in
  let task_prepared = Driver.prepare_task driver task 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 command = Re.replace_string nnet_or_onnx ~by:nn_file command in
  let prover_call =
    Driver.prove_task_prepared ~command ~limit driver task_prepared
  in
  let prover_result = Call_provers.wait_on_call prover_call in
  Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
    Call_provers.print_prover_answer prover_result.pr_answer

let verify format loadpath ?memlimit ~prover file =
  let open Why3 in
  (* Debug.(set_flag (lookup_flag "call_prover")); *)
  let env, config = create_env loadpath in
  let steplimit = None in
  let timeout = 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 =
        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 prover driver) tasks)
    mstr_theory