autodetection.ml 9.57 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
(*    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
23
open Ident
24 25 26
open Whyconf
open Rc

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

(* 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;
41
      versions_bad : string list;
42 43 44
      prover_command : string;
      prover_driver : string;
      prover_editor : string;
45
      prover_in_place : bool;
46 47 48 49 50 51
    }

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

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";
65
    versions_bad = get_stringl section ~default:[] "version_bad";
66 67 68
    prover_command = get_string section "command";
    prover_driver = get_string section "driver";
    prover_editor = get_string section ~default:"" "editor";
69
    prover_in_place = get_bool section ~default:false "in_place";
70 71
  }

72 73 74 75 76 77 78
let editor_keys =
  let add acc k = Sstr.add k acc in
  List.fold_left add Sstr.empty
    ["command"]

let load_editor section =
  check_exhaustive section prover_keys;
MARCHE Claude's avatar
MARCHE Claude committed
79 80
  { editor_name = get_string section "name";
    editor_command = get_string section "command";
81 82 83
    editor_options = []
  }

84
(** returned in reverse order *)
85 86
let load rc =
  let atps = get_family rc "ATP" in
87
  let atps = List.rev_map (load_prover ATP) atps in
88 89 90 91 92
  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 =
93 94
  let filename = Filename.concat (Whyconf.datadir main)
    "provers-detection-data.conf" in
95 96 97 98 99
  try
    let rc = Rc.from_file filename in
    load rc
  with
    | Failure "lexing" ->
100
        Loc.errorm "Syntax error in provers-detection-data.conf@."
101
    | Not_found ->
102
        Loc.errorm "provers-detection-data.conf not found at %s@." filename
103 104 105 106 107

let provers_found = ref 0

let prover_tips_info = ref false

108 109 110 111 112 113 114 115 116 117 118 119 120
let read_editors main =
  let filename = Filename.concat (Whyconf.datadir main)
    "provers-detection-data.conf" in
  try
    let rc = Rc.from_file filename in
    List.fold_left (fun editors (id, section) ->
      Meditor.add id (load_editor section) editors
    ) Meditor.empty (get_family rc "editor")
  with
    | Failure "lexing" ->
        Loc.errorm "Syntax error in provers-detection-data.conf@."
    | Not_found ->
        Loc.errorm "provers-detection-data.conf not found at %s@." filename
121 122 123 124 125 126 127 128 129

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

130 131 132
let sanitize_exec =
  let first c = match c with
    | '_' | ' ' -> "_"
133
    | _ -> char_to_alpha c
134 135 136
  in
  let rest c = match c with
    | '+' | '-' | '.' -> String.make 1 c
137
    | _ -> char_to_alnumus c
138
  in
139
  sanitizer first rest
140

141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
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;
158
        Sys.remove out;
159 160 161 162 163 164 165 166 167 168 169 170
        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
171
          eprintf "Found prover %s version %s, OK.@." nam ver
172 173 174 175 176 177 178
        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
179
            else
180 181 182 183
              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
184 185 186 187 188
        let prover = {Whyconf.prover_name = data.prover_name;
                      prover_version = ver;
                      prover_altern = ""} in
        Some {prover = prover;
              id = data.prover_id;
189 190
              command = c;
              driver  = Filename.concat (datadir main) data.prover_driver;
191
              editor = data.prover_editor;
192
              in_place = data.prover_in_place;
193 194 195
              interactive = (match data.kind with ITP -> true | ATP -> false);
              extra_options = [];
              extra_drivers = [] }
196 197 198 199
      end
    with Not_found ->
      begin
        prover_tips_info := true;
200
        eprintf "Warning: found prover %s but name/version not \
201
                       recognized by regexp `%s'@."
202
          data.prover_name data.version_regexp;
203 204
        eprintf "Answer was `%s'@." s;
        None
205 206 207 208 209 210
      end

let detect_prover main acc l =
  try
    let detect_execs data =
      try Some (Util.list_first (detect_exec main data) data.execs)
211 212
      with Not_found -> None
    in
213
    let prover = Util.list_first detect_execs l in
214
    Mprover.add prover.prover prover acc
215
  with Not_found ->
216
    eprintf "Prover %s not found.@." (List.hd l).prover_id;
217
    acc
218 219 220 221 222 223 224 225 226 227 228 229
(* 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
*)
230 231 232 233

let run_auto_detection config =
  let main = get_main config in
  let l = read_auto_detection_data main in
234 235
  let cmp p q = String.compare p.prover_id q.prover_id in
  let l = Util.list_part cmp l in
236 237
  let detect = List.fold_left (detect_prover main) Mprover.empty l in
  let length = Mprover.cardinal detect in
238
  eprintf "%d provers detected.@." length;
239
  set_provers (set_editors config (read_editors main)) detect
240 241 242 243 244 245 246 247

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

248 249 250 251 252 253 254 255 256 257 258 259
let get_altern id path =
  let alt = Filename.basename path in
  let ilen = String.length id in
  let alen = String.length alt in
  let rec get_suffix i =
    if i = alen then "alt" else
    if i = ilen then String.sub alt i (alen-i) else
    if id.[i] = alt.[i] then get_suffix (i+1) else
    String.sub alt i (alen-i)
  in
  get_suffix 0

260 261 262 263 264 265 266 267 268 269
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
270 271 272 273 274 275 276 277
  (* alternative name *)
  let alt = get_altern id path in
  let provers = get_provers config in
  (* is a prover with this name and version already in config? *)
  let p = if not (Mprover.mem p.prover provers) then p else
    { p with prover = { p.prover with prover_altern = alt } } in
  let alt = sanitizer char_to_alnumus char_to_alnumus alt in
  let p = { p with id = p.id ^ "-" ^ alt } in
278
  set_provers config (Mprover.add p.prover p (get_provers config))