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 stdlib = Dirs.Sites.stdlib in
  let open Why3 in
  ( Env.create_env
      (loadpath @ stdlib @ Whyconf.loadpath (Whyconf.get_main config)),
    config )

let verify format loadpath prover file =
  let open Why3 in
  let env, config = create_env loadpath 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 tasks ~f:(Fmt.pr "%a" (Driver.print_task driver)))
    mstr_theory