autodetection.ml 21.9 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
(*****
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
31
detected. If a message is not present, we print ", OK." if the version
32 33 34 35 36 37
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
open Format
François Bobot's avatar
François Bobot committed
43
open Stdlib
44
open Whyconf
45
module Wc = Whyconf
46 47
open Rc

48
let debug = Debug.register_info_flag "autodetect"
Andrei Paskevich's avatar
Andrei Paskevich committed
49 50
  ~desc:"Print@ debugging@ messages@ about@ auto-detection@ \
         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
      compile_time_support : bool;
61 62 63
      execs : string list;
      version_switch : string;
      version_regexp : string;
MARCHE Claude's avatar
MARCHE Claude committed
64 65 66
      versions_ok : (string * Str.regexp) list;
      versions_old : (string * Str.regexp) list;
      versions_bad : (string * Str.regexp) list;
67 68
      (** If none it's a fake prover (very bad version) *)
      prover_command : string option;
69
      prover_command_steps : string option;
70 71
      prover_driver : string;
      prover_editor : string;
72
      prover_in_place : bool;
73
      use_at_auto_level : int;
74
      message : string option;
75 76 77 78 79
    }

let prover_keys =
  let add acc k = Sstr.add k acc in
  List.fold_left add Sstr.empty
80 81
    ["name";"compile_time_support";
     "exec";"version_switch";"version_regexp";
82
     "version_ok";"version_old";"version_bad";"command"; "command_steps";
83
     "editor";"driver";"in_place";"message";"alternative";"use_at_auto_level"]
84 85 86

let load_prover kind (id,section) =
  check_exhaustive section prover_keys;
MARCHE Claude's avatar
MARCHE Claude committed
87
  let reg_map = List.rev_map (fun s -> (s,why3_regexp_of_string s)) in
88
  let prover = { kind = kind;
89 90
    prover_id = id;
    prover_name = get_string section "name";
91
    prover_altern = get_string section ~default:"" "alternative";
92
    compile_time_support =
93
      get_bool section ~default:false "compile_time_support";
94 95 96
    execs = get_stringl section "exec";
    version_switch = get_string section ~default:"" "version_switch";
    version_regexp = get_string section ~default:"" "version_regexp";
97 98 99
    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");
100
    prover_command = get_stringo section "command";
101
    prover_command_steps = get_stringo section "command_steps";
102
    prover_driver = get_string section ~default:""  "driver";
103
    prover_editor = get_string section ~default:"" "editor";
104
    prover_in_place = get_bool section ~default:false "in_place";
105
    use_at_auto_level = get_int section ~default:0 "use_at_auto_level";
106
    message = get_stringo section "message";
107 108 109 110 111
  } in
  if prover.prover_command != None && prover.prover_driver = "" then
    invalid_arg
      (sprintf "In section prover %s command specified without driver" id);
  prover
112

113
(* dead code
114 115 116 117
let editor_keys =
  let add acc k = Sstr.add k acc in
  List.fold_left add Sstr.empty
    ["command"]
118
*)
119 120 121

let load_editor section =
  check_exhaustive section prover_keys;
MARCHE Claude's avatar
MARCHE Claude committed
122 123
  { editor_name = get_string section "name";
    editor_command = get_string section "command";
124 125 126
    editor_options = []
  }

127
(** returned in reverse order *)
128 129
let load rc =
  let atps = get_family rc "ATP" in
130
  let atps = List.rev_map (load_prover ATP) atps in
131
  let itps = get_family rc "ITP" in
132
  let tps = List.fold_left (Lists.cons (load_prover ITP)) atps itps in
133 134
  tps

135 136 137 138 139 140 141 142 143 144
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

145 146 147 148 149
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
150

151 152
type env =
  {
153
    (* memoization of (exec_name,version_switch)
154
        -> Some output | None doesn't exists *)
François Bobot's avatar
François Bobot committed
155
    prover_output : string option Hstr2.t;
156
    (* existing executable table:
François Bobot's avatar
François Bobot committed
157 158
        exec_name -> | Some (priority, id, prover_config)
                                  unknown version (neither good or bad)
159
                     | None               there is a good version *)
François Bobot's avatar
François Bobot committed
160
    prover_unknown_version :
MARCHE Claude's avatar
MARCHE Claude committed
161
      (prover_autodetection_data * int * string * config_prover) option Hstr.t;
162
    (* string -> priority * prover  *)
François Bobot's avatar
François Bobot committed
163
    prover_shortcuts : (int * prover) Hstr.t;
164 165 166 167
    mutable possible_prover_shortcuts : (filter_prover * string) list;
  }

let create_env shortcuts =
François Bobot's avatar
François Bobot committed
168 169 170
{ prover_output = Hstr2.create 10;
  prover_unknown_version = Hstr.create 10;
  prover_shortcuts = Hstr.create 5;
171 172 173
  possible_prover_shortcuts = shortcuts;
 }

François Bobot's avatar
François Bobot committed
174 175 176 177 178 179
let next_priority =
  let r = ref 0 in
  fun () -> decr r; !r

let highest_priority = 0

180
let read_auto_detection_data main =
181 182
  let filename = Filename.concat (Whyconf.datadir main)
    "provers-detection-data.conf" in
183 184
  try
    let rc = Rc.from_file filename in
185 186 187
    let shortcuts =
      List.fold_left load_prover_shortcut [] (get_family rc "shortcut") in
    List.rev (load rc), create_env shortcuts
188 189
  with
    | Failure "lexing" ->
190
        Loc.errorm "Syntax error in provers-detection-data.conf@."
191
    | Not_found ->
192
        Loc.errorm "provers-detection-data.conf not found at %s@." filename
193

194 195 196 197 198 199 200 201 202 203 204 205 206
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
207

208
let make_command =
209
  let cmd_regexp = Str.regexp "%\\(.\\)" in
210 211 212 213 214 215
  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
216

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

230
let ask_prover_version exec_name version_switch =
231
  let out = Filename.temp_file "out" "" in
232
  let cmd = sprintf "%s %s" exec_name version_switch in
233
  let c = sprintf "(%s) >%s 2>&1" cmd out in
234
  Debug.dprintf debug "Run : %s@." c;
235 236 237 238 239 240 241 242
  try
    let ret = Sys.command c in
    let ch = open_in out in
    let c = Sysutil.channel_contents ch in
    close_in ch;
    Sys.remove out;
    if ret <> 0 then begin
      Debug.dprintf debug "command '%s' failed. Output:@\n%s@." cmd c;
243
      None
244 245 246 247
    end else Some c
  with Not_found | End_of_file | Sys_error _ ->
    Debug.dprintf debug "command '%s' failed@." cmd;
    None
248 249 250

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

MARCHE Claude's avatar
MARCHE Claude committed
257
let check_version version (_,schema) = Str.string_match schema version 0
258 259

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

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


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
285 286 287
    (* start with 2 in order to have toto_alt, toto_alt2,
       toto_alt3,... and not toto_alt, toto_alt1 which can be
       confusing *)
288 289 290
    aux 2

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

296 297 298 299
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
300
      Hstr.replace env.prover_shortcuts s (highest_priority,prover);
301 302 303 304
      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
305
let add_id_prover_shortcut env id prover priority =
306
  match Hstr.find_opt env.prover_shortcuts id with
François Bobot's avatar
François Bobot committed
307
  | Some (p,_) when p >= priority -> ()
308
(*
309
  | Some _ -> assert false
310
 *)
François Bobot's avatar
François Bobot committed
311 312
  | _ -> Hstr.replace env.prover_shortcuts id (priority,prover)

313 314 315 316 317 318 319 320 321 322 323 324 325 326 327
let prover_auto_levels = Hprover.create 5

let record_prover_for_auto_mode prover level =
  Hprover.replace prover_auto_levels prover (level,false)

let check_prover_auto_level prover =
  try
    let lev,_ = Hprover.find prover_auto_levels prover in
    Hprover.replace prover_auto_levels prover (lev,true)
  with Not_found -> ()

let generate_auto_strategies config =
  eprintf "Generating strategies:@.";
  Hprover.iter
    (fun p (lev,b) ->
328 329
     if b then eprintf "  Prover %a will be used in Auto level >= %d@."
                       Whyconf.print_prover p lev) prover_auto_levels;
330 331 332 333 334 335 336 337
  (* Split *)
  let code = "t split_goal_wp exit" in
  let split = {
      strategy_name = "Split";
      strategy_desc = "Split@ the@ goal@ into@ subgoals";
      strategy_shortcut = "s";
      strategy_code = code }
  in
338 339 340 341 342 343 344 345
  (* Inline *)
  let code = "t introduce_premises next next: t inline_goal exit" in
  let inline = {
      strategy_name = "Inline";
      strategy_desc = "Inline@ definitions@ in@ the@ conclusion@ of@ the@ goal";
      strategy_shortcut = "i";
      strategy_code = code }
  in
346
  (* Auto level 0 and 1 *)
347 348 349 350
  let provers_level1 =
    Hprover.fold
      (fun p (lev,b) acc ->
       if b && lev = 1 then
MARCHE Claude's avatar
MARCHE Claude committed
351
         let name = Whyconf.prover_parseable_format p in name :: acc
352 353
       else acc) prover_auto_levels []
  in
354 355 356
  List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level1;
  let code = flush_str_formatter () in
  let auto0 = {
MARCHE Claude's avatar
MARCHE Claude committed
357
      strategy_name = "Auto_level_0";
358 359 360 361
      strategy_desc = "Automatic@ run@ of@ main@ provers";
      strategy_shortcut = "0";
      strategy_code = code }
  in
362 363 364 365 366 367
  fprintf str_formatter "start:@\n";
  List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level1;
  fprintf str_formatter "t split_goal_wp start@\n";
  List.iter (fun s -> fprintf str_formatter "c %s 10 4000@\n" s) provers_level1;
  let code = flush_str_formatter () in
  let auto1 = {
MARCHE Claude's avatar
MARCHE Claude committed
368
      strategy_name = "Auto_level_1";
369 370 371 372 373 374 375 376 377
      strategy_desc = "Automatic@ run@ of@ main@ provers";
      strategy_shortcut = "1";
      strategy_code = code }
  in
  (* Auto level 2 *)
  let provers_level2 =
    Hprover.fold
      (fun p (lev,b) acc ->
       if b && lev >= 1 && lev <= 2 then
MARCHE Claude's avatar
MARCHE Claude committed
378
         let name = Whyconf.prover_parseable_format p in name :: acc
379 380 381 382 383 384 385 386 387
       else acc) prover_auto_levels []
  in
  fprintf str_formatter "start:@\n";
  List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level2;
  fprintf str_formatter "t split_goal_wp start@\n";
  List.iter (fun s -> fprintf str_formatter "c %s 5 2000@\n" s) provers_level2;
  fprintf str_formatter "t introduce_premises afterintro@\n";
  fprintf str_formatter "afterintro:@\n";
  fprintf str_formatter "t inline_goal afterinline@\n";
388
  fprintf str_formatter "g trylongertime@\n";
389 390
  fprintf str_formatter "afterinline:@\n";
  fprintf str_formatter "t split_goal_wp start@\n";
391
  fprintf str_formatter "trylongertime:@\n";
392 393 394
  List.iter (fun s -> fprintf str_formatter "c %s 30 4000@\n" s) provers_level2;
  let code = flush_str_formatter () in
  let auto2 = {
MARCHE Claude's avatar
MARCHE Claude committed
395
      strategy_name = "Auto_level_2";
396 397 398 399
      strategy_desc = "Automatic@ run@ of@ provers@ and@ most@ useful@ transformations";
      strategy_shortcut = "2";
      strategy_code = code }
  in
400 401
  add_strategy
    (add_strategy
402 403 404 405
       (add_strategy
          (add_strategy
             (add_strategy config inline)
             split) auto0) auto1) auto2
406

407
let detect_exec env data acc exec_name =
408 409 410 411 412 413
  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 =
414 415
    try
      ignore (Str.search_forward re s 0);
416
      Str.matched_group 1 s
417 418
    with Not_found ->
      begin
419
        Debug.dprintf debug "Warning: found prover %s but name/version not \
420
                       recognized by regexp `%s'@."
421
          data.prover_name data.version_regexp;
422 423 424 425
        Debug.dprintf debug "Answer was `%s'@." s;
        ""
      end
  in
426 427
  (* bad mean here not good, it's not the same thing than a version
     of a prover with known problems *)
428 429 430
  let bad = List.exists (check_version ver) data.versions_bad in
  if bad then (known_version env exec_name; acc)
  else
431 432 433
    (* check if this prover needs compile-time support *)
    let missing_compile_time_support =
      if data.compile_time_support then
434
        try
435
          let compile_time_ver =
436 437
            List.assoc data.prover_name Config.compile_time_support
          in
438
          if compile_time_ver <> ver then begin
439
            eprintf
440 441 442 443 444 445 446
              "Found prover %s version %s, but Why3 was compiled with support for version %s@."
            data.prover_name ver compile_time_ver;
            true
          end
          else
            false
        with Not_found ->
447
          eprintf
448 449 450 451 452 453 454 455
            "Found prover %s version %s, but Why3 wasn't compiled with support for it@."
            data.prover_name ver;
          true
      else false
    in
    if missing_compile_time_support then
      (known_version env exec_name; acc)
    else
456 457 458 459
    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 ->
460
      (* Empty prover *)
461
      if good || old then begin (* Known version with error *)
462 463 464
        known_version env exec_name;
        eprintf "Found prover %s version %s%s@."
          data.prover_name ver
465
          (Opt.get_def
466 467 468
             ". This version of the prover is known to have problems."
             data.message);
        acc
469
      end
470
      else (* it's not a known bad version *) acc
471

472
    | Some prover_command ->
473
    (* create the prover config *)
474
    let c = make_command exec_name prover_command in
475 476 477 478
    let c_steps = (match data.prover_command_steps with
      | None -> None
      | Some prover_command_steps ->
	Some (make_command exec_name prover_command_steps)) in
479 480 481 482 483 484
    let prover = {Wc.prover_name = data.prover_name;
                  prover_version      = ver;
                  prover_altern       = data.prover_altern} in
    let prover_config =
      {prover  = prover;
       command = c;
485
       command_steps = c_steps;
486
       driver  = data.prover_driver;
487
       editor  = data.prover_editor;
488
       in_place  = data.prover_in_place;
489 490 491 492
       interactive   = (match data.kind with ITP -> true | ATP -> false);
       extra_options = [];
       extra_drivers = [] } in

François Bobot's avatar
François Bobot committed
493
    let priority = next_priority () in
494 495 496
    if good || old then begin
      eprintf "Found prover %s version %s%s@."
        data.prover_name ver
497 498 499 500 501 502 503 504
        (Opt.get_def
	   (if old then
	      " (old version, please consider upgrading)."
	    else
	      if data.prover_altern <> "" then
		" (alternative: " ^ data.prover_altern ^ ")"
	      else
		", OK.")
505 506
           data.message);
      known_version env exec_name;
507
      add_prover_shortcuts env prover;
François Bobot's avatar
François Bobot committed
508
      add_id_prover_shortcut env data.prover_id prover priority;
509 510
      let level = data.use_at_auto_level in
      if level > 0 then record_prover_for_auto_mode prover level;
511 512
      add_prover_with_uniq_id prover_config acc
    end
MARCHE Claude's avatar
MARCHE Claude committed
513
    else (unknown_version env exec_name data.prover_id prover_config data priority;
François Bobot's avatar
François Bobot committed
514
          acc)
515

516 517
let detect_prover env acc data =
  List.fold_left (detect_exec env data) acc data.execs
518

MARCHE Claude's avatar
MARCHE Claude committed
519 520 521 522
let pp_versions =
  Pp.print_list Pp.comma
                (Pp.print_pair_delim Pp.nothing Pp.nothing Pp.nothing Pp.string Pp.nothing)

523 524
(** add the prover unknown *)
let detect_unknown env detected =
François Bobot's avatar
François Bobot committed
525
  Hstr.fold (fun _ pc acc ->
526 527
    match pc with
    | None -> acc
MARCHE Claude's avatar
MARCHE Claude committed
528
    | Some (prover_data,priority,prover_id,prover_config) ->
529
      let prover = prover_config.prover in
MARCHE Claude's avatar
MARCHE Claude committed
530 531 532 533 534 535
      Warning.emit "@[Prover %s version %s is not known to be supported.@\n\
                    Known versions for this prover:@ %a@\n\
                    Known old versions for this prover:@ %a@]@."
                   prover.Wc.prover_name prover.prover_version
                   pp_versions prover_data.versions_ok
                   pp_versions prover_data.versions_old;
536 537 538 539
      (* 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. *)
François Bobot's avatar
François Bobot committed
540
      add_id_prover_shortcut env prover_id prover priority;
541 542
      add_prover_with_uniq_id prover_config acc)
    env.prover_unknown_version detected
543

544
let convert_shortcuts env =
François Bobot's avatar
François Bobot committed
545
  Hstr.fold (fun s (_,p) acc ->
546
    check_prover_auto_level p; Mstr.add s p acc
547 548
  ) env.prover_shortcuts Mstr.empty

549 550
let run_auto_detection config =
  let main = get_main config in
551
  let l,env = read_auto_detection_data main in
552
  let detected = List.fold_left (detect_prover env) Mprover.empty l in
553 554 555 556
  let length_detected = Mprover.cardinal detected in
  let detected = detect_unknown env detected in
  let length_unsupported_version =
    Mprover.cardinal detected - length_detected in
557 558 559
  eprintf
    "%d provers detected and %d provers detected with unsupported version@."
    length_detected length_unsupported_version;
560
  let shortcuts = convert_shortcuts env in
561
  let config = generate_auto_strategies config in
562 563 564 565
  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
566 567

let list_prover_ids () =
568
  let config = default_config "" in
569
  let main = get_main config in
570
  let l,_ = read_auto_detection_data main in
571 572 573
  let s = List.fold_left (fun s p -> Sstr.add p.prover_id s) Sstr.empty l in
  Sstr.elements s

574
let get_suffix id alt =
575 576
  let ilen = String.length id in
  let alen = String.length alt in
577
  let rec aux i =
578 579
    if i = alen then "alt" else
    if i = ilen then String.sub alt i (alen-i) else
580
    if id.[i] = alt.[i] then aux (i+1) else
581 582
    String.sub alt i (alen-i)
  in
583 584 585 586 587 588
  aux 0


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

590 591
let add_existing_shortcuts env shortcuts =
  let aux shortcut prover =
François Bobot's avatar
François Bobot committed
592
    Hstr.replace env.prover_shortcuts shortcut (highest_priority,prover);
593
    env.possible_prover_shortcuts <-
François Bobot's avatar
François Bobot committed
594 595
      List.filter (fun (_,s) -> s = shortcut)
      env.possible_prover_shortcuts
596 597 598
  in
  Mstr.iter aux shortcuts

599 600
let add_prover_binary config id path =
  let main = get_main config in
601 602
  let l,env = read_auto_detection_data main in
  add_existing_shortcuts env (get_prover_shortcuts config);
603 604
  let l = List.filter (fun p -> p.prover_id = id) l in
  if l = [] then Loc.errorm "Unknown prover id: %s" id;
605
  let detected = List.fold_left
606
    (fun acc data -> detect_exec env data acc path) Mprover.empty l in
607 608 609
  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;
610
  let provers = get_provers config in
611
  let fold _ p provers =
612
    (* find a prover altern not used *)
613 614 615
    (* 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
616 617 618
        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
619
        find_prover_altern provers prover_id in
620 621
    let p = {p with prover = prover_id} in
    add_prover_with_uniq_id p provers in
622
  let provers = Mprover.fold fold detected provers in
623
  let shortcuts = convert_shortcuts env in
624
  let config = set_provers config ~shortcuts provers in
625
  config