verification.ml

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

open Base
module Filename = Caml.Filename

let () = Language.register_nnet_support ()
let () = Language.register_onnx_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 : Why3.Whyconf.config_prover) driver task =
  let open Why3 in
  let task_prepared = Driver.prepare_task driver task in
  let tasks =
    if String.equal prover.prover.prover_name "Marabou"
    then
      let conjs = Trans.apply Split_goal.split_goal_full task_prepared in
      let disjs =
        List.map ~f:(Trans.apply Split_disjunction.split_disjunction) conjs
      in
      disjs
    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 command = Re.replace_string nnet_or_onnx ~by:nn_file command in
  let call_task task_prepared =
    let prover_call =
      Driver.prove_task_prepared ~command ~limit driver task_prepared
    in
    let prover_result = Call_provers.wait_on_call prover_call in
    prover_result.pr_answer
  in
  let results = List.map tasks ~f:(List.map ~f:call_task) in
  let answer =
    List.fold_left results ~init:Call_provers.Valid ~f:(fun r1 l2 ->
      let r2 =
        List.fold_left l2 ~init:Call_provers.Invalid ~f:(fun r1 r2 ->
          match (r1, r2) with
          | Call_provers.Valid, _ | _, Call_provers.Valid -> Call_provers.Valid
          | _ -> r2)
      in
      match (r1, r2) with
      | Call_provers.Valid, r | r, Call_provers.Valid -> r
      | _ -> r1)
  in
  Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
    Call_provers.print_prover_answer 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