autodetection.ml 16.5 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
(*****
1) For every block, for every executable call the prover using the
version switch and add the prover to the configuration if the version
match one of the version_ok or version_old but none of the version_bad
2) We consider that an executable name which appears in a block, but
which version isn't a version_ok, version_old or version_bad has an
unknown version
3) For every executable which have an unknown version, we add the
prover using the first block that contains it.

Don't use the family argument except when you add manualy one prover.

So the order of the block is used only when the version of an
executable appears in none of the block.

A block with more than one exec fields is now the same thing than if you
split the block into blocks containing one fields.

New message field that allows to print a message when a prover is
detected. If a message is not present, we print ", Ok." if the version
is good (version_good) and not old, and " (it is an old version)." if
the version is old (version_old).

The field command can be missing in a block, in that case the block
defines a version known to be buggy: no prover config is generated.

38 39
The regexp must start with ^.

40 41
*)

42 43 44
open Format
open Util
open Whyconf
François Bobot's avatar
François Bobot committed
45
open Stdlib
46
module Wc = Whyconf
47 48
open Rc

49
let debug = Debug.register_info_flag "autodetect"
50
  ~desc:"About@ the@ autodetection@ of@ external@ provers."
51 52 53 54 55 56 57 58

(* auto-detection of provers *)

type prover_kind = ATP | ITP
type prover_autodetection_data =
    { kind : prover_kind;
      prover_id : string;
      prover_name : string;
59
      prover_altern : string;
60 61 62
      execs : string list;
      version_switch : string;
      version_regexp : string;
63 64 65
      versions_ok : Str.regexp list;
      versions_old : Str.regexp list;
      versions_bad : Str.regexp list;
66 67
      (** If none it's a fake prover (very bad version) *)
      prover_command : string option;
68 69
      prover_driver : string;
      prover_editor : string;
70
      prover_in_place : bool;
71
      message : string option;
72 73 74 75 76 77
    }

let prover_keys =
  let add acc k = Sstr.add k acc in
  List.fold_left add Sstr.empty
    ["name";"exec";"version_switch";"version_regexp";
78
     "version_ok";"version_old";"version_bad";"command";
79
     "editor";"driver";"in_place";"message"]
80 81 82

let load_prover kind (id,section) =
  check_exhaustive section prover_keys;
83
  let reg_map = List.rev_map why3_regexp_of_string in
84
  let prover = { kind = kind;
85 86
    prover_id = id;
    prover_name = get_string section "name";
87
    prover_altern = get_string section ~default:"" "altern";
88 89 90
    execs = get_stringl section "exec";
    version_switch = get_string section ~default:"" "version_switch";
    version_regexp = get_string section ~default:"" "version_regexp";
91 92 93
    versions_ok = reg_map $ get_stringl section ~default:[] "version_ok";
    versions_old = reg_map $ get_stringl section ~default:[] "version_old";
    versions_bad = reg_map $ get_stringl section ~default:[] "version_bad";
94
    prover_command = get_stringo section "command";
95
    prover_driver = get_string section ~default:""  "driver";
96
    prover_editor = get_string section ~default:"" "editor";
97
    prover_in_place = get_bool section ~default:false "in_place";
98
    message = get_stringo section "message";
99 100 101 102 103
  } in
  if prover.prover_command != None && prover.prover_driver = "" then
    invalid_arg
      (sprintf "In section prover %s command specified without driver" id);
  prover
104

105
(* dead code
106 107 108 109
let editor_keys =
  let add acc k = Sstr.add k acc in
  List.fold_left add Sstr.empty
    ["command"]
110
*)
111 112 113

let load_editor section =
  check_exhaustive section prover_keys;
MARCHE Claude's avatar
MARCHE Claude committed
114 115
  { editor_name = get_string section "name";
    editor_command = get_string section "command";
116 117 118
    editor_options = []
  }

119
(** returned in reverse order *)
120 121
let load rc =
  let atps = get_family rc "ATP" in
122
  let atps = List.rev_map (load_prover ATP) atps in
123
  let itps = get_family rc "ITP" in
124
  let tps = List.fold_left (Lists.cons (load_prover ITP)) atps itps in
125 126
  tps

127 128 129 130 131 132 133 134 135 136
let load_prover_shortcut acc (_, section) =
  let name = get_string section "name" in
  let version = get_stringo section "version" in
  let altern = get_stringo section "alternative" in
  let shortcuts = get_stringl section "shortcut" in
  let fp = mk_filter_prover ?version ?altern name in
  List.fold_left (fun acc shortcut ->
    (fp,shortcut)::acc
  ) acc shortcuts

137 138 139 140 141
module Hstr2 = Hashtbl.Make(struct
  type t = string * string
  let hash = Hashtbl.hash
  let equal = (=)
end)
François Bobot's avatar
François Bobot committed
142

143 144 145 146
type env =
  {
    (** memoization of (exec_name,version_switch)
        -> Some output | None doesn't exists *)
François Bobot's avatar
François Bobot committed
147
    prover_output : string option Hstr2.t;
148
    (** existing executable table:
François Bobot's avatar
François Bobot committed
149 150
        exec_name -> | Some (priority, id, prover_config)
                                  unknown version (neither good or bad)
151
                     | None               there is a good version *)
François Bobot's avatar
François Bobot committed
152 153 154 155
    prover_unknown_version :
      (int * string * config_prover) option Hstr.t;
    (** string -> priority * prover  *)
    prover_shortcuts : (int * prover) Hstr.t;
156 157 158 159
    mutable possible_prover_shortcuts : (filter_prover * string) list;
  }

let create_env shortcuts =
François Bobot's avatar
François Bobot committed
160 161 162
{ prover_output = Hstr2.create 10;
  prover_unknown_version = Hstr.create 10;
  prover_shortcuts = Hstr.create 5;
163 164 165
  possible_prover_shortcuts = shortcuts;
 }

François Bobot's avatar
François Bobot committed
166 167 168 169 170 171
let next_priority =
  let r = ref 0 in
  fun () -> decr r; !r

let highest_priority = 0

172
let read_auto_detection_data main =
173 174
  let filename = Filename.concat (Whyconf.datadir main)
    "provers-detection-data.conf" in
175 176
  try
    let rc = Rc.from_file filename in
177 178 179
    let shortcuts =
      List.fold_left load_prover_shortcut [] (get_family rc "shortcut") in
    List.rev (load rc), create_env shortcuts
180 181
  with
    | Failure "lexing" ->
182
        Loc.errorm "Syntax error in provers-detection-data.conf@."
183
    | Not_found ->
184
        Loc.errorm "provers-detection-data.conf not found at %s@." filename
185

186
(* dead code
187
let provers_found = ref 0
188
*)
189

190 191 192 193 194 195 196 197 198 199 200 201 202
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
203

204
let make_command =
205
  let cmd_regexp = Str.regexp "%\\(.\\)" in
206 207 208 209 210 211
  fun exec com ->
    let replace s = match Str.matched_group 1 s with
      | "e" -> exec
      | c -> "%"^c
    in
    Str.global_substitute cmd_regexp replace com
212

213
(* dead code
214 215 216
let sanitize_exec =
  let first c = match c with
    | '_' | ' ' -> "_"
217
    | _ -> char_to_alpha c
218 219 220
  in
  let rest c = match c with
    | '+' | '-' | '.' -> String.make 1 c
221
    | _ -> char_to_alnumus c
222
  in
223
  sanitizer first rest
224
*)
225

226
let ask_prover_version exec_name version_switch =
227
  let out = Filename.temp_file "out" "" in
228
  let cmd = sprintf "%s %s" exec_name version_switch in
229 230 231 232 233 234 235 236 237
  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
238 239 240 241 242 243 244 245 246 247
    try
      let ch = open_in out in
      let c = Sysutil.channel_contents ch in
      close_in ch;
      Sys.remove out;
      Some c
    with Not_found | End_of_file  -> Some ""

let ask_prover_version env exec_name version_switch =
  try
François Bobot's avatar
François Bobot committed
248
    Hstr2.find env.prover_output (exec_name,version_switch)
249 250
  with Not_found ->
    let res = ask_prover_version exec_name version_switch in
François Bobot's avatar
François Bobot committed
251
    Hstr2.add env.prover_output (exec_name,version_switch) res;
252 253
    res

254
let check_version version schema = Str.string_match schema version 0
255 256

let known_version env exec_name =
François Bobot's avatar
François Bobot committed
257
  Hstr.replace env.prover_unknown_version exec_name None
258

François Bobot's avatar
François Bobot committed
259 260 261 262
let unknown_version env exec_name prover_id prover_config priority =
  if not (Hstr.mem env.prover_unknown_version exec_name)
  then Hstr.replace env.prover_unknown_version exec_name
    (Some (priority,prover_id,prover_config))
263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290


let empty_alt s = if s = "" then "alt" else s

let find_prover_altern provers prover_id =
  if not (Mprover.mem prover_id provers) then prover_id
  else
    let prover_id =
      {prover_id with
        Wc.prover_altern = empty_alt prover_id.Wc.prover_altern} in
    if not (Mprover.mem prover_id provers) then prover_id
    else
    let rec aux n =
      let prover_id_n = {prover_id with
        Wc.prover_altern = sprintf "%s_%i"
          (empty_alt prover_id.Wc.prover_altern) n} in
      if Mprover.mem prover_id_n provers
      then aux (n+1)
      else prover_id_n in
    (** start with 2 in order to have toto_alt, toto_alt2,
        toto_alt3,... and not toto_alt, toto_alt1 which can be
        confusing *)
    aux 2

let add_prover_with_uniq_id prover provers =
  (** find an unique prover triplet *)
  let prover_id = find_prover_altern provers prover.Wc.prover in
  let prover = {prover with Wc.prover = prover_id} in
291
  Mprover.add prover_id prover provers
292

293 294 295 296
let add_prover_shortcuts env prover =
  let rec aux = function
    | [] -> []
    | (fp,s)::l when filter_prover fp prover ->
François Bobot's avatar
François Bobot committed
297
      Hstr.replace env.prover_shortcuts s (highest_priority,prover);
298 299 300 301
      aux l
    | a::l -> a::(aux l) in
  env.possible_prover_shortcuts <- aux env.possible_prover_shortcuts

François Bobot's avatar
François Bobot committed
302
let add_id_prover_shortcut env id prover priority =
303
  match Hstr.find_opt env.prover_shortcuts id with
François Bobot's avatar
François Bobot committed
304 305 306
  | Some (p,_) when p >= priority -> ()
  | _ -> Hstr.replace env.prover_shortcuts id (priority,prover)

307

308 309 310 311 312 313 314
let detect_exec env main data acc exec_name =
  let s = ask_prover_version env exec_name data.version_switch in
  match s with
  | None -> acc
  | Some s ->
  let re = Str.regexp data.version_regexp in
  let ver =
315 316
    try
      ignore (Str.search_forward re s 0);
317
      Str.matched_group 1 s
318 319
    with Not_found ->
      begin
320
        Debug.dprintf debug "Warning: found prover %s but name/version not \
321
                       recognized by regexp `%s'@."
322
          data.prover_name data.version_regexp;
323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341
        Debug.dprintf debug "Answer was `%s'@." s;
        ""
      end
  in
  (** bad mean here not good, it's not the same thing than a version
      of a prover with known problems *)
  let bad = List.exists (check_version ver) data.versions_bad in
  if bad then (known_version env exec_name; acc)
  else

    let good = List.exists (check_version ver) data.versions_ok in
    let old  = List.exists (check_version ver) data.versions_old in
    match data.prover_command with
    | None ->
      (** Empty prover *)
      if good || old then begin (** Known version with error *)
        known_version env exec_name;
        eprintf "Found prover %s version %s%s@."
          data.prover_name ver
342
          (Opt.get_def
343 344 345
             ". This version of the prover is known to have problems."
             data.message);
        acc
346
      end
347
      else (** it's not a known bad version *) acc
348

349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364
    | Some prover_command ->
    (** create the prover config *)
    let c = make_command exec_name prover_command in
    let prover = {Wc.prover_name = data.prover_name;
                  prover_version      = ver;
                  prover_altern       = data.prover_altern} in
    let prover_config =
      {prover  = prover;
       command = c;
       driver  = Filename.concat (datadir main) data.prover_driver;
       editor  = data.prover_editor;
       in_place      = data.prover_in_place;
       interactive   = (match data.kind with ITP -> true | ATP -> false);
       extra_options = [];
       extra_drivers = [] } in

François Bobot's avatar
François Bobot committed
365
    let priority = next_priority () in
366 367 368
    if good || old then begin
      eprintf "Found prover %s version %s%s@."
        data.prover_name ver
369
        (Opt.get_def (if old then
370 371
            " (it is an old version that is less tested than \
             the current one)." else ", Ok.")
372 373
           data.message);
      known_version env exec_name;
374
      add_prover_shortcuts env prover;
François Bobot's avatar
François Bobot committed
375
      add_id_prover_shortcut env data.prover_id prover priority;
376 377
      add_prover_with_uniq_id prover_config acc
    end
François Bobot's avatar
François Bobot committed
378 379
    else (unknown_version env exec_name data.prover_id prover_config priority;
          acc)
380 381 382 383 384 385

let detect_prover env main acc data =
  List.fold_left (detect_exec env main data) acc data.execs

(** add the prover unknown *)
let detect_unknown env detected =
François Bobot's avatar
François Bobot committed
386
  Hstr.fold (fun _ pc acc ->
387 388
    match pc with
    | None -> acc
François Bobot's avatar
François Bobot committed
389
    | Some (priority,prover_id,prover_config) ->
390 391 392 393
      let prover = prover_config.prover in
      eprintf "Warning: prover %s version %s is not known to be \
                     supported, use it at your own risk!@."
        prover.Wc.prover_name prover.prover_version;
François Bobot's avatar
François Bobot committed
394 395 396 397 398
      (** Pb: Even if it match the first prover section (normally
          highest priority) since it is unknown it has the lower
          priority for its id as shortcut. Perhaps we don't want
          that. *)
      add_id_prover_shortcut env prover_id prover priority;
399 400
      add_prover_with_uniq_id prover_config acc)
    env.prover_unknown_version detected
401

402
let convert_shortcuts env =
François Bobot's avatar
François Bobot committed
403
  Hstr.fold (fun s (_,p) acc ->
404 405 406
    Mstr.add s p acc
  ) env.prover_shortcuts Mstr.empty

407 408
let run_auto_detection config =
  let main = get_main config in
409 410 411 412 413 414
  let l,env = read_auto_detection_data main in
  let detected = List.fold_left (detect_prover env main) Mprover.empty l in
  let length_detected = Mprover.cardinal detected in
  let detected = detect_unknown env detected in
  let length_unsupported_version =
    Mprover.cardinal detected - length_detected in
415 416 417
  eprintf
    "%d provers detected and %d provers detected with unsupported version@."
    length_detected length_unsupported_version;
418 419 420 421 422
  let shortcuts = convert_shortcuts env in
  let config = set_editors config (read_editors main) in
  let config = set_prover_shortcuts config shortcuts in
  let config = set_provers config detected in
  config
423 424

let list_prover_ids () =
425
  let config = default_config "" in
426
  let main = get_main config in
427
  let l,_ = read_auto_detection_data main in
428 429 430
  let s = List.fold_left (fun s p -> Sstr.add p.prover_id s) Sstr.empty l in
  Sstr.elements s

431
let get_suffix id alt =
432 433
  let ilen = String.length id in
  let alen = String.length alt in
434
  let rec aux i =
435 436
    if i = alen then "alt" else
    if i = ilen then String.sub alt i (alen-i) else
437
    if id.[i] = alt.[i] then aux (i+1) else
438 439
    String.sub alt i (alen-i)
  in
440 441 442 443 444 445
  aux 0


let get_altern id path =
  let alt = Filename.basename path in
  get_suffix id alt
446

447 448
let add_existing_shortcuts env shortcuts =
  let aux shortcut prover =
François Bobot's avatar
François Bobot committed
449
    Hstr.replace env.prover_shortcuts shortcut (highest_priority,prover);
450
    env.possible_prover_shortcuts <-
François Bobot's avatar
François Bobot committed
451 452
      List.filter (fun (_,s) -> s = shortcut)
      env.possible_prover_shortcuts
453 454 455
  in
  Mstr.iter aux shortcuts

456 457
let add_prover_binary config id path =
  let main = get_main config in
458 459
  let l,env = read_auto_detection_data main in
  add_existing_shortcuts env (get_prover_shortcuts config);
460 461
  let l = List.filter (fun p -> p.prover_id = id) l in
  if l = [] then Loc.errorm "Unknown prover id: %s" id;
462 463 464 465 466
  let detected = List.fold_left
    (fun acc data -> detect_exec env main data acc path) Mprover.empty l in
  let detected = detect_unknown env detected in
  if Mprover.is_empty detected then
    Loc.errorm "File %s does not correspond to the prover id %s" path id;
467
  let provers = get_provers config in
468 469 470 471 472
  let fold _ p provers =
    (** find a prover altern not used *)
    (* Is a prover with this name and version already in config? *)
    let prover_id =
      if not (Mprover.mem p.prover provers) then p.prover else
473 474 475
        let alt = match p.prover.Wc.prover_altern, get_altern id path with
          | "", s -> s | s, "" -> s | s1, s2 -> s1 ^ " " ^ s2 in
        let prover_id = { p.prover with Wc.prover_altern = alt } in
476
        find_prover_altern provers prover_id in
477 478
    let p = {p with prover = prover_id} in
    add_prover_with_uniq_id p provers in
479
  let provers = Mprover.fold fold detected provers in
480
  let shortcuts = convert_shortcuts env in
481
  let config = set_provers config ~shortcuts provers in
482
  config