autodetection.ml 6.65 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 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103
  try
    let rc = Rc.from_file filename in
    load rc
  with
    | Failure "lexing" ->
        eprintf "Syntax error in provers-detection-data.conf@.";
        exit 2
    | Not_found ->
        eprintf "provers-detection-data.conf not found at %s@." filename;
        exit 2


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

104 105 106 107 108 109 110 111 112 113 114
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

115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131
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;
132
        Sys.remove out;
133 134 135 136 137 138 139 140 141 142 143 144
        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
145
          eprintf "Found prover %s version %s, OK.@." nam ver
146 147 148 149 150 151 152
        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
153
            else
154 155 156 157 158 159 160 161
              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
        Some {name = data.prover_name;
              version = ver;
              command = c;
              driver  = Filename.concat (datadir main) data.prover_driver;
162 163
              editor = data.prover_editor;
              interactive = match data.kind with ITP -> true | ATP -> false; }
164 165 166 167
      end
    with Not_found ->
      begin
        prover_tips_info := true;
168
        eprintf "Warning: found prover %s but name/version not \
169
                       recognized by regexp `%s'@."
170
          data.prover_name data.version_regexp;
171 172
        eprintf "Answer was `%s'@." s;
        None
173 174 175 176 177 178 179 180 181 182 183 184 185
      end

let detect_prover main acc l =
  let prover_id = (List.hd l).prover_id in
  try
    let detect_execs data =
      try Some (Util.list_first (detect_exec main data) data.execs)
      with Not_found -> None in
    let prover = Util.list_first detect_execs l in
    Mstr.add prover_id prover acc
  with Not_found ->
    eprintf "Prover %s not found.@." prover_id;
    acc
186 187 188 189

let run_auto_detection config =
  let main = get_main config in
  let l = read_auto_detection_data main in
190 191
  let cmp p q = String.compare p.prover_id q.prover_id in
  let l = Util.list_part cmp l in
192
  let detect = List.fold_left (detect_prover main) Mstr.empty l in
François Bobot's avatar
François Bobot committed
193
  let length = Mstr.cardinal detect in
194 195
  eprintf "%d provers detected.@." length;
  set_provers config detect