autodetection.ml 17.7 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   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 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
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;
64 65 66
      versions_ok : Str.regexp list;
      versions_old : Str.regexp list;
      versions_bad : 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
      message : string option;
74 75 76 77 78
    }

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

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

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

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

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

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

143 144 145 146 147
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
148

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

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

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

let highest_priority = 0

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

192
(* dead code
193
let provers_found = ref 0
194
*)
195

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

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

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

232
let ask_prover_version exec_name version_switch =
233
  let out = Filename.temp_file "out" "" in
234
  let cmd = sprintf "%s %s" exec_name version_switch in
235 236 237 238 239 240 241 242 243
  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
244 245 246 247 248 249 250 251 252 253
    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
254
    Hstr2.find env.prover_output (exec_name,version_switch)
255 256
  with Not_found ->
    let res = ask_prover_version exec_name version_switch in
François Bobot's avatar
François Bobot committed
257
    Hstr2.add env.prover_output (exec_name,version_switch) res;
258 259
    res

260
let check_version version schema = Str.string_match schema version 0
261 262

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

François Bobot's avatar
François Bobot committed
265 266 267 268
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))
269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287


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

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

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

313

314 315 316 317 318 319 320
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 =
321 322
    try
      ignore (Str.search_forward re s 0);
323
      Str.matched_group 1 s
324 325
    with Not_found ->
      begin
326
        Debug.dprintf debug "Warning: found prover %s but name/version not \
327
                       recognized by regexp `%s'@."
328
          data.prover_name data.version_regexp;
329 330 331 332
        Debug.dprintf debug "Answer was `%s'@." s;
        ""
      end
  in
333 334
  (* bad mean here not good, it's not the same thing than a version
     of a prover with known problems *)
335 336 337
  let bad = List.exists (check_version ver) data.versions_bad in
  if bad then (known_version env exec_name; acc)
  else
338 339 340
    (* check if this prover needs compile-time support *)
    let missing_compile_time_support =
      if data.compile_time_support then
341
        try
342
          let compile_time_ver =
343 344
            List.assoc data.prover_name Config.compile_time_support
          in
345
          if compile_time_ver <> ver then begin
346
            eprintf
347 348 349 350 351 352 353
              "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 ->
354
          eprintf
355 356 357 358 359 360 361 362
            "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
363 364 365 366
    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 ->
367
      (* Empty prover *)
368
      if good || old then begin (* Known version with error *)
369 370 371
        known_version env exec_name;
        eprintf "Found prover %s version %s%s@."
          data.prover_name ver
372
          (Opt.get_def
373 374 375
             ". This version of the prover is known to have problems."
             data.message);
        acc
376
      end
377
      else (* it's not a known bad version *) acc
378

379
    | Some prover_command ->
380
    (* create the prover config *)
381
    let c = make_command exec_name prover_command in
382 383 384 385
    let c_steps = (match data.prover_command_steps with
      | None -> None
      | Some prover_command_steps ->
	Some (make_command exec_name prover_command_steps)) in
386 387 388 389 390 391
    let prover = {Wc.prover_name = data.prover_name;
                  prover_version      = ver;
                  prover_altern       = data.prover_altern} in
    let prover_config =
      {prover  = prover;
       command = c;
392
       command_steps = c_steps;
393 394 395 396 397 398 399
       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
400
    let priority = next_priority () in
401 402 403
    if good || old then begin
      eprintf "Found prover %s version %s%s@."
        data.prover_name ver
404
        (Opt.get_def (if old then
405
            " (old version, please consider upgrading)." else ", Ok.")
406 407
           data.message);
      known_version env exec_name;
408
      add_prover_shortcuts env prover;
François Bobot's avatar
François Bobot committed
409
      add_id_prover_shortcut env data.prover_id prover priority;
410 411
      add_prover_with_uniq_id prover_config acc
    end
François Bobot's avatar
François Bobot committed
412 413
    else (unknown_version env exec_name data.prover_id prover_config priority;
          acc)
414 415 416 417 418 419

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
420
  Hstr.fold (fun _ pc acc ->
421 422
    match pc with
    | None -> acc
François Bobot's avatar
François Bobot committed
423
    | Some (priority,prover_id,prover_config) ->
424
      let prover = prover_config.prover in
425
      Warning.emit "Warning: prover %s version %s is not known to be \
426
                     supported.@."
427
        prover.Wc.prover_name prover.prover_version;
428 429 430 431
      (* 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
432
      add_id_prover_shortcut env prover_id prover priority;
433 434
      add_prover_with_uniq_id prover_config acc)
    env.prover_unknown_version detected
435

436
let convert_shortcuts env =
François Bobot's avatar
François Bobot committed
437
  Hstr.fold (fun s (_,p) acc ->
438 439 440
    Mstr.add s p acc
  ) env.prover_shortcuts Mstr.empty

441 442
let run_auto_detection config =
  let main = get_main config in
443 444 445 446 447 448
  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
449 450 451
  eprintf
    "%d provers detected and %d provers detected with unsupported version@."
    length_detected length_unsupported_version;
452 453 454 455 456
  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
457 458

let list_prover_ids () =
459
  let config = default_config "" in
460
  let main = get_main config in
461
  let l,_ = read_auto_detection_data main in
462 463 464
  let s = List.fold_left (fun s p -> Sstr.add p.prover_id s) Sstr.empty l in
  Sstr.elements s

465
let get_suffix id alt =
466 467
  let ilen = String.length id in
  let alen = String.length alt in
468
  let rec aux i =
469 470
    if i = alen then "alt" else
    if i = ilen then String.sub alt i (alen-i) else
471
    if id.[i] = alt.[i] then aux (i+1) else
472 473
    String.sub alt i (alen-i)
  in
474 475 476 477 478 479
  aux 0


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

481 482
let add_existing_shortcuts env shortcuts =
  let aux shortcut prover =
François Bobot's avatar
François Bobot committed
483
    Hstr.replace env.prover_shortcuts shortcut (highest_priority,prover);
484
    env.possible_prover_shortcuts <-
François Bobot's avatar
François Bobot committed
485 486
      List.filter (fun (_,s) -> s = shortcut)
      env.possible_prover_shortcuts
487 488 489
  in
  Mstr.iter aux shortcuts

490 491
let add_prover_binary config id path =
  let main = get_main config in
492 493
  let l,env = read_auto_detection_data main in
  add_existing_shortcuts env (get_prover_shortcuts config);
494 495
  let l = List.filter (fun p -> p.prover_id = id) l in
  if l = [] then Loc.errorm "Unknown prover id: %s" id;
496 497 498 499 500
  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;
501
  let provers = get_provers config in
502
  let fold _ p provers =
503
    (* find a prover altern not used *)
504 505 506
    (* 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
507 508 509
        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
510
        find_prover_altern provers prover_id in
511 512
    let p = {p with prover = prover_id} in
    add_prover_with_uniq_id p provers in
513
  let provers = Mprover.fold fold detected provers in
514
  let shortcuts = convert_shortcuts env in
515
  let config = set_provers config ~shortcuts provers in
516
  config