autodetection.ml 7.82 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software 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.                  *)
(*                                                                        *)
(**************************************************************************)

open Format
open Util
open Whyconf
open Rc

25
let debug = Debug.register_flag "autodetect"
26 27 28 29 30 31 32 33 34 35 36 37 38

(* auto-detection of provers *)

type prover_kind = ATP | ITP
type prover_autodetection_data =
    { kind : prover_kind;
      prover_id : string;
      prover_name : string;
      execs : string list;
      version_switch : string;
      version_regexp : string;
      versions_ok : string list;
      versions_old : string list;
39
      versions_bad : string list;
40 41 42 43 44 45 46 47 48
      prover_command : string;
      prover_driver : string;
      prover_editor : string;
    }

let prover_keys =
  let add acc k = Sstr.add k acc in
  List.fold_left add Sstr.empty
    ["name";"exec";"version_switch";"version_regexp";
49
     "version_ok";"version_old";"version_bad";"command";
50 51 52 53 54 55 56 57 58 59 60 61
     "editor";"driver"]

let load_prover kind (id,section) =
  check_exhaustive section prover_keys;
  { kind = kind;
    prover_id = id;
    prover_name = get_string section "name";
    execs = get_stringl section "exec";
    version_switch = get_string section ~default:"" "version_switch";
    version_regexp = get_string section ~default:"" "version_regexp";
    versions_ok = get_stringl section ~default:[] "version_ok";
    versions_old = get_stringl section ~default:[] "version_old";
62
    versions_bad = get_stringl section ~default:[] "version_bad";
63 64 65 66 67
    prover_command = get_string section "command";
    prover_driver = get_string section "driver";
    prover_editor = get_string section ~default:"" "editor";
  }

68
(** returned in reverse order *)
69 70
let load rc =
  let atps = get_family rc "ATP" in
71
  let atps = List.rev_map (load_prover ATP) atps in
72 73 74 75 76
  let itps = get_family rc "ITP" in
  let tps = List.fold_left (cons (load_prover ITP)) atps itps in
  tps

let read_auto_detection_data main =
77 78
  let filename = Filename.concat (Whyconf.datadir main)
    "provers-detection-data.conf" in
79 80 81 82 83
  try
    let rc = Rc.from_file filename in
    load rc
  with
    | Failure "lexing" ->
84
        Loc.errorm "Syntax error in provers-detection-data.conf@."
85
    | Not_found ->
86
        Loc.errorm "provers-detection-data.conf not found at %s@." filename
87 88 89 90 91 92 93 94 95 96 97 98 99 100

let provers_found = ref 0

let prover_tips_info = ref false


let make_command exec com =
  let cmd_regexp = Str.regexp "%\\(.\\)" in
  let replace s = match Str.matched_group 1 s with
    | "e" -> exec
    | c -> "%"^c
  in
  Str.global_substitute cmd_regexp replace com

101 102 103 104 105 106 107 108 109 110 111
let sanitize_exec =
  let first c = match c with
    | '_' | ' ' -> "_"
    | _ -> Ident.char_to_alpha c
  in
  let rest c = match c with
    | '+' | '-' | '.' -> String.make 1 c
    | _ -> Ident.char_to_alnumus c
  in
  Ident.sanitizer first rest

112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
let detect_exec main data com =
  let out = Filename.temp_file "out" "" in
  let cmd = sprintf "%s %s" com data.version_switch in
  let c = sprintf "(%s) > %s 2>&1" cmd out in
  Debug.dprintf debug "Run : %s@." c;
  let ret = Sys.command c in
  if ret <> 0 then
    begin
      Debug.dprintf debug "command '%s' failed@." cmd;
      None
    end
  else
    let s =
      try
        let ch = open_in out in
        let c = Sysutil.channel_contents ch in
        close_in ch;
129
        Sys.remove out;
130 131 132 133 134 135 136 137 138 139 140 141
        c
      with Not_found | End_of_file  -> ""
    in
    let re = Str.regexp data.version_regexp in
    try
      ignore (Str.search_forward re s 0);
      let nam = data.prover_name in
      let ver = Str.matched_group 1 s in
      if List.mem ver data.versions_bad then
        None
      else begin
        if List.mem ver data.versions_ok then
142
          eprintf "Found prover %s version %s, OK.@." nam ver
143 144 145 146 147 148 149
        else
          begin
            prover_tips_info := true;
            if List.mem ver data.versions_old then
              eprintf "Warning: prover %s version %s is quite old, please \
                     consider upgrading to a newer version.@."
                nam ver
150
            else
151 152 153 154
              eprintf "Warning: prover %s version %s is not known to be \
                     supported, use it at your own risk!@." nam ver
          end;
        let c = make_command com data.prover_command in
155 156 157 158 159
        let prover = {Whyconf.prover_name = data.prover_name;
                      prover_version = ver;
                      prover_altern = ""} in
        Some {prover = prover;
              id = data.prover_id;
160 161
              command = c;
              driver  = Filename.concat (datadir main) data.prover_driver;
162
              editor = data.prover_editor;
163 164 165
              interactive = (match data.kind with ITP -> true | ATP -> false);
              extra_options = [];
              extra_drivers = [] }
166 167 168 169
      end
    with Not_found ->
      begin
        prover_tips_info := true;
170
        eprintf "Warning: found prover %s but name/version not \
171
                       recognized by regexp `%s'@."
172
          data.prover_name data.version_regexp;
173 174
        eprintf "Answer was `%s'@." s;
        None
175 176 177 178 179 180
      end

let detect_prover main acc l =
  try
    let detect_execs data =
      try Some (Util.list_first (detect_exec main data) data.execs)
181 182
      with Not_found -> None
    in
183
    let prover = Util.list_first detect_execs l in
184
    Mprover.add prover.prover prover acc
185
  with Not_found ->
186
    eprintf "Prover %s not found.@." (List.hd l).prover_id;
187
    acc
188 189 190 191 192 193 194 195 196 197 198 199
(* does not work
  List.fold_left
    (fun acc data ->
      List.fold_left
        (fun acc e ->
          eprintf "Trying executable %s@." e;
          match detect_exec main data e with
            | None -> acc
            | Some prover -> Mstr.add prover_id prover acc)
        acc data.execs)
    acc l
*)
200 201 202 203

let run_auto_detection config =
  let main = get_main config in
  let l = read_auto_detection_data main in
204 205
  let cmp p q = String.compare p.prover_id q.prover_id in
  let l = Util.list_part cmp l in
206 207
  let detect = List.fold_left (detect_prover main) Mprover.empty l in
  let length = Mprover.cardinal detect in
208 209
  eprintf "%d provers detected.@." length;
  set_provers config detect
210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228

let list_prover_ids () =
  let config = default_config "/dev/null" in
  let main = get_main config in
  let l = read_auto_detection_data main in
  let s = List.fold_left (fun s p -> Sstr.add p.prover_id s) Sstr.empty l in
  Sstr.elements s

let add_prover_binary config id path =
  let main = get_main config in
  let l = read_auto_detection_data main in
  let l = List.filter (fun p -> p.prover_id = id) l in
  if l = [] then Loc.errorm "Unknown prover id: %s" id;
  let p = try
    Util.list_first (fun d -> detect_exec main d path) (List.rev l)
  with Not_found ->
    Loc.errorm "File %s does not correspond to the prover id %s" path id
  in
  set_provers config (Mprover.add p.prover p (get_provers config))