whyconf.ml 17.8 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
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
20 21

open Format
22
open Util
23
open Rc
24
open Stdlib
25

26 27
(* magicnumber for the configuration :
  - 0 before the magic number
28
  - 1 when no loadpath meant default loadpath
29 30
  - 2
  - 5 cvc3 native
Andrei Paskevich's avatar
Andrei Paskevich committed
31
  - 6 driver renaming
32
  - 7 yices native (used for release 0.70)
33
  - 8 for release 0.71
34
  - 9 coq realizations
35
  - 10 require %f in editor lines
36
  - 11 change prover identifiers in provers-detection-data.conf
37
  - 12 split editors out of provers
38

39
If a configuration doesn't contain the actual magic number we don't use it.*)
40

41
let magicnumber = 12
42

43 44
exception WrongMagicNumber

45 46
(* lib and shared dirs *)

47 48 49
let default_loadpath =
  [ Filename.concat Config.datadir "theories";
    Filename.concat Config.datadir "modules"; ]
MARCHE Claude's avatar
MARCHE Claude committed
50

51
let default_conf_file =
52
  match Config.localdir with
53 54
    | None -> Filename.concat (Rc.get_home_dir ()) ".why3.conf"
    | Some d -> Filename.concat d "why3.conf"
55

56 57 58
(* Prover *)

type prover =
59
    { prover_name : string;
60
      prover_version : string;
61
      prover_altern : string;
62 63 64
    }

let print_prover fmt p =
65 66 67 68
  Format.fprintf fmt "%s (%s)" p.prover_name p.prover_version
  (* Format.fprintf fmt "%s (%s%s%s)" *)
  (*   p.prover_name p.prover_version *)
  (*   (if p.prover_altern = "" then "" else " ") p.prover_altern *)
69 70 71 72 73 74 75 76

module Prover = struct
  type t = prover
  let compare s1 s2 =
    if s1 == s2 then 0 else
    let c = String.compare s1.prover_name s2.prover_name in
    if c <> 0 then c else
    let c = String.compare s1.prover_version s2.prover_version in
77 78
    (* if c <> 0 then c else *)
    (* let c = String.compare s1.prover_altern s2.prover_altern in *)
79 80 81
    c

  let equal s1 s2 =
82 83
    s1 == s2 ||
      (s1.prover_name = s2.prover_name &&
84 85
       s1.prover_version = s2.prover_version(*  && *)
       (* s1.prover_altern = s2.prover_altern *))
86 87

  let hash s1 =
88
      2 * Hashtbl.hash s1.prover_name +
89 90
      3 * Hashtbl.hash s1.prover_version (* + *)
      (* 5 * Hashtbl.hash s1.prover_altern *)
91 92 93 94 95 96
end

module Mprover = Map.Make(Prover)
module Sprover = Mprover.Set
module Hprover = Hashtbl.Make(Prover)

97 98 99 100 101 102 103
module Editor = struct
  type t = string
  let compare = Pervasives.compare
end

module Meditor = Map.Make(Editor)

104 105
(* Configuration file *)

106 107 108 109 110
type prover_upgrade_policy =
  | CPU_keep
  | CPU_upgrade of prover
  | CPU_duplicate of prover

111
type config_prover = {
112 113 114 115
  prover  : prover;
  id      : string;
  command : string;
  driver  : string;
116
  in_place: bool;
117
  editor  : string;
118
  interactive : bool;
119 120
  extra_options : string list;
  extra_drivers : string list;
121 122
}

123
type config_editor = {
MARCHE Claude's avatar
MARCHE Claude committed
124
  editor_name : string;
125 126 127 128
  editor_command : string;
  editor_options : string list;
}

129

130
type main = {
131 132
  libdir   : string;      (* "/usr/local/lib/why/" *)
  datadir  : string;      (* "/usr/local/share/why/" *)
133
  loadpath  : string list;  (* "/usr/local/lib/why/theories" *)
134 135
  timelimit : int;
  (* default prover time limit in seconds (0 unlimited) *)
136
  memlimit  : int;
137
  (* default prover memory limit in megabytes (0 unlimited)*)
138
  running_provers_max : int;
139
  (* max number of running prover processes *)
François Bobot's avatar
François Bobot committed
140
  plugins : string list;
141
  (* plugins to load, without extension, relative to [libdir]/plugins *)
142 143
}

MARCHE Claude's avatar
MARCHE Claude committed
144 145 146
let libdir m =
  try
    Sys.getenv "WHY3LIB"
147
  with Not_found -> m.libdir
MARCHE Claude's avatar
MARCHE Claude committed
148 149 150

let datadir m =
  try
151 152 153 154 155
    let d = Sys.getenv "WHY3DATA" in
(*
    eprintf "[Info] datadir set using WHY3DATA='%s'@." d;
*)
    d
156
  with Not_found -> m.datadir
MARCHE Claude's avatar
MARCHE Claude committed
157

158
let loadpath m =
159 160 161 162 163
  try
    let d = Sys.getenv "WHY3LOADPATH" in
(*
    eprintf "[Info] loadpath set using WHY3LOADPATH='%s'@." d;
*)
164
    Str.split (Str.regexp ":") d
165 166 167 168 169 170 171 172 173
  with Not_found -> m.loadpath

let timelimit m = m.timelimit
let memlimit m = m.memlimit
let running_provers_max m = m.running_provers_max

let set_limits m time mem running =
  { m with timelimit = time; memlimit = mem; running_provers_max = running }

François Bobot's avatar
François Bobot committed
174 175 176 177
let plugins m = m.plugins
let set_plugins m pl =
  (* TODO : sanitize? *)
  { m with plugins = pl}
178

François Bobot's avatar
François Bobot committed
179 180 181 182 183
let add_plugin m p =
  if List.mem p m.plugins
  then m
  else { m with plugins = List.rev (p::(List.rev m.plugins))}

Andrei Paskevich's avatar
Andrei Paskevich committed
184
let pluginsdir m = Filename.concat m.libdir "plugins"
François Bobot's avatar
François Bobot committed
185 186
let load_plugins m =
  let load x =
187
    try Plugin.load x
188 189 190
    with exn ->
      Format.eprintf "%s can't be loaded : %a@." x
        Exn_printer.exn_printer exn in
François Bobot's avatar
François Bobot committed
191 192
  List.iter load m.plugins

193
type config = {
194
  conf_file : string;       (* "/home/innocent_user/.why3.conf" *)
195
  config    : Rc.t;
196
  main      : main;
197
  provers   : config_prover Mprover.t;
198
  editors   : config_editor Meditor.t;
199
  provers_upgrade_policy : prover_upgrade_policy Mprover.t;
200 201
}

202 203
let default_main =
  {
204 205 206
    libdir = Config.libdir;
    datadir = Config.datadir;
    loadpath = default_loadpath;
207 208 209
    timelimit = 5;   (* 5 seconds *)
    memlimit = 1000; (* 1 Mb *)
    running_provers_max = 2; (* two provers run in parallel *)
François Bobot's avatar
François Bobot committed
210
    plugins = [];
211
  }
212

213
let set_main rc main =
214
  let section = empty_section in
215
  let section = set_int section "magic" magicnumber in
216 217 218 219 220
  let section = set_string ~default:default_main.libdir
    section "libdir" main.libdir in
  let section = set_string ~default:default_main.datadir
    section "datadir" main.datadir in
  let section = set_stringl section "loadpath" main.loadpath in
221 222 223 224
  let section = set_int section "timelimit" main.timelimit in
  let section = set_int section "memlimit" main.memlimit in
  let section =
    set_int section "running_provers_max" main.running_provers_max in
François Bobot's avatar
François Bobot committed
225
  let section = set_stringl section "plugin" main.plugins in
226
  set_section rc "main" section
227

228 229 230 231
exception NonUniqueId

let set_prover _ prover (ids,family) =
  if Sstr.mem prover.id ids then raise NonUniqueId;
232
  let section = empty_section in
233
  let section = set_string section "name" prover.prover.prover_name in
234 235
  let section = set_string section "command" prover.command in
  let section = set_string section "driver" prover.driver in
236
  let section = set_string section "version" prover.prover.prover_version in
237
  let section = set_string ~default:"" section "alternative" prover.prover.prover_altern in
238
  let section = set_string section "editor" prover.editor in
239
  let section = set_bool section "interactive" prover.interactive in
240
  let section = set_bool section "in_place" prover.in_place in
241
  (Sstr.add prover.id ids,(prover.id,section)::family)
242

243
let set_provers rc provers =
244
  let _,family = Mprover.fold set_prover provers (Sstr.empty,[]) in
245
  set_family rc "prover" family
246

247 248 249
let set_editor id editor (ids, family) =
  if Sstr.mem id ids then raise NonUniqueId;
  let section = empty_section in
MARCHE Claude's avatar
MARCHE Claude committed
250
  let section = set_string section "name" editor.editor_name in
251 252 253 254 255 256 257
  let section = set_string section "command" editor.editor_command in
  (Sstr.add id ids, (id, section)::family)

let set_editors rc editors =
  let _,family = Meditor.fold set_editor editors (Sstr.empty,[]) in
  set_family rc "editor" family

258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285
let set_prover_upgrade_policy prover policy (i, family) =
  let section = empty_section in
  let section = set_string section "name" prover.prover_name in
  let section = set_string section "version" prover.prover_version in
  let section = set_string section "alternative" prover.prover_altern in
  let section =
    match policy with
      | CPU_keep -> 
        set_string section "policy" "keep"
      | CPU_upgrade p ->
        let section = set_string section "target_name" p.prover_name in
        let section = set_string section "target_version" p.prover_version in
        let section = set_string section "target_alternative" p.prover_altern in
        set_string section "policy" "upgrade"
      | CPU_duplicate p ->
        let section = set_string section "target_name" p.prover_name in
        let section = set_string section "target_version" p.prover_version in
        let section = set_string section "target_alternative" p.prover_altern in
        set_string section "policy" "duplicate"
  in
  (i+1,("policy" ^ string_of_int i, section)::family)

let set_policies rc policy =
  let _,family =
    Mprover.fold set_prover_upgrade_policy policy (0,[])
  in
  set_family rc "uninstalled_prover" family

286
let absolute_filename = Sysutil.absolutize_filename
287

288
let load_prover dirname provers (id,section) =
289
  let name = get_string section "name" in
290
  let version = get_string ~default:"" section "version" in
291
  let altern = get_string ~default:"" section "alternative" in
292
  let prover =
293 294
    { prover_name = name;
      prover_version = version;
295 296
      prover_altern = altern;
    }
297 298
  in
  Mprover.add prover
299 300
    { id = id;
      prover  = prover;
301 302
      command = get_string section "command";
      driver  = absolute_filename dirname (get_string section "driver");
303
      in_place = get_bool ~default:false section "in_place";
304
      editor  = get_string ~default:"" section "editor";
305
      interactive = get_bool ~default:false section "interactive";
306 307
      extra_options = [];
      extra_drivers = [];
308 309
    } provers

310 311
let load_editor editors (id, section) =
  Meditor.add id
MARCHE Claude's avatar
MARCHE Claude committed
312 313
    { editor_name = get_string ~default:id section "name";
      editor_command = get_string section "command";
314 315 316
      editor_options = [];
    } editors

317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346
let load_policy provers acc (_,section) =
  let source =
    {prover_name = get_string section "name";
     prover_version = get_string section "version";
     prover_altern = get_string ~default:"" section "alternative"
    } in
  try
    match get_string section "policy" with
      | "keep" -> Mprover.add source CPU_keep acc
      | "upgrade" ->
        let target =
          { prover_name = get_string section "target_name";
            prover_version = get_string section "target_version";
            prover_altern = get_string ~default:"" section "target_alternative";
          }
        in
        let _target = Mprover.find target provers in
        Mprover.add source (CPU_upgrade target) acc
      | "duplicate" -> 
        let target =
          { prover_name = get_string section "target_name";
            prover_version = get_string section "target_version";
            prover_altern = get_string ~default:"" section "target_alternative";
          }
        in
        let _target = Mprover.find target provers in
        Mprover.add source (CPU_duplicate target) acc
      | _ -> raise Not_found
  with Not_found -> acc

347
let load_main dirname section =
348 349
  if get_int ~default:0 section "magic" <> magicnumber then
    raise WrongMagicNumber;
350 351
  { libdir    = get_string ~default:default_main.libdir section "libdir";
    datadir   = get_string ~default:default_main.datadir section "datadir";
352
    loadpath  = List.map (absolute_filename dirname)
353
      (get_stringl ~default:[] section "loadpath");
354 355
    timelimit = get_int ~default:default_main.timelimit section "timelimit";
    memlimit  = get_int ~default:default_main.memlimit section "memlimit";
356 357
    running_provers_max = get_int ~default:default_main.running_provers_max
      section "running_provers_max";
François Bobot's avatar
François Bobot committed
358
    plugins = get_stringl ~default:[] section "plugin";
359 360
  }

361
let read_config_rc conf_file =
362 363
  let filename = match conf_file with
    | Some filename -> filename
364
    | None -> begin try Sys.getenv "WHY3CONFIG" with Not_found ->
365 366
          if Sys.file_exists default_conf_file then default_conf_file
          else raise Exit
367 368
        end
  in
369 370 371 372 373
  filename, Rc.from_file filename

exception ConfigFailure of string (* filename *) * string

let () = Exn_printer.register (fun fmt e -> match e with
374
  | ConfigFailure (f, s) ->
375
      Format.fprintf fmt "error in config file %s: %s" f s
376 377
  | WrongMagicNumber ->
      Format.fprintf fmt "outdated config file; rerun why3config"
378 379
  | NonUniqueId ->
    Format.fprintf fmt "InternalError : two provers share the same id"
380
  | _ -> raise e)
381 382 383 384 385

let get_config (filename,rc) =
  let dirname = Filename.dirname filename in
  let rc, main =
    match get_section rc "main" with
386
      | None      -> raise (ConfigFailure (filename, "no main section"))
387
      | Some main -> rc, load_main dirname main
388
  in
389
  let provers = get_family rc "prover" in
390
  let provers = List.fold_left (load_prover dirname) Mprover.empty provers in
391 392
  let editors = get_family rc "editor" in
  let editors = List.fold_left load_editor Meditor.empty editors in
393 394
  let policy = get_family rc "uninstalled_prover" in
  let policy = List.fold_left (load_policy provers) Mprover.empty policy in
395
  { conf_file = filename;
396 397 398
    config    = rc;
    main      = main;
    provers   = provers;
399
    editors   = editors;
400
    provers_upgrade_policy = policy;
401
  }
402

403
let default_config conf_file =
404
  get_config (conf_file, set_main Rc.empty default_main)
405

406
let read_config conf_file =
407 408
  let filenamerc =
    try
409
      read_config_rc conf_file
410
    with Exit ->
411 412
      default_conf_file, set_main Rc.empty default_main
  in
413
  try
414
    get_config filenamerc
415 416 417 418
  with e when not (Debug.test_flag Debug.stack_trace) ->
    let b = Buffer.create 40 in
    Format.bprintf b "%a" Exn_printer.exn_printer e;
    raise (ConfigFailure (fst filenamerc, Buffer.contents b))
419

420 421 422 423 424 425 426 427 428 429 430 431 432
let merge_config config filename =
  let dirname = Filename.dirname filename in
  let rc = Rc.from_file filename in
  let main = match get_section rc "main" with
    | None -> config.main
    | Some rc ->
      let loadpath = (List.map (absolute_filename dirname)
        (get_stringl ~default:[] rc "loadpath")) @ config.main.loadpath in
      let plugins = (get_stringl ~default:[] rc "plugin") @ config.main.plugins in
      { config.main with loadpath = loadpath; plugins = plugins } in
  let provers = get_family rc "prover" in
  let provers = List.fold_left
    (fun provers (id, section) ->
433 434
      try
        let key,c = Mprover.choose (Mprover.filter (fun _ p -> p.id = id) provers) in
435 436 437
        let opt = (get_stringl ~default:[] section "option") @ c.extra_options in
        let drv = (List.map (absolute_filename dirname)
          (get_stringl ~default:[] section "driver")) @ c.extra_options in
438 439 440
        Mprover.add key { c with extra_options = opt ; extra_drivers = drv } provers
      with
        Not_found -> load_prover dirname provers (id, section)
441
    ) config.provers provers in
442 443 444 445 446 447 448 449 450 451 452
  let editors = get_family rc "editor" in
  let editors = List.fold_left
    (fun editors (id, section) ->
      try
        let c = Meditor.find id editors in
        let opt = (get_stringl ~default:[] section "option") @ c.editor_options in
        Meditor.add id { c with editor_options = opt } editors
      with
        Not_found -> load_editor editors (id, section)
    ) config.editors editors in
  { config with main = main; provers = provers; editors = editors }
453

454
let save_config config =
455
  let filename = config.conf_file in
456
  Sysutil.backup_file filename;
457
  to_file filename config.config
458

459 460
let get_main config = config.main
let get_provers config = config.provers
461 462 463
let get_policies config = config.provers_upgrade_policy
let get_prover_upgrade_policy config p =
  Mprover.find p config.provers_upgrade_policy
464

465 466 467 468
let set_main config main =
  {config with
    config = set_main config.config main;
    main = main;
469 470
  }

471 472 473 474 475
let set_provers config provers =
  {config with
    config = set_provers config.config provers;
    provers = provers;
  }
476

477 478 479 480 481 482
let set_editors config editors =
  { config with
    config = set_editors config.config editors;
    editors = editors;
  }

483 484 485 486 487 488 489 490 491 492 493 494 495 496
let set_prover_upgrade_policy config prover target =
  let m = Mprover.add prover target config.provers_upgrade_policy in
  {config with
    config = set_policies config.config m;
    provers_upgrade_policy = m;
  }

let set_policies config policies = 
  { config with
    config = set_policies config.config policies;
    provers_upgrade_policy = policies }



497 498
(*******)

499
let set_conf_file config conf_file = {config with conf_file = conf_file}
500
let get_conf_file config           =  config.conf_file
501

502 503 504 505 506 507 508 509 510
(*******)

let is_prover_known whyconf prover =
  Mprover.mem prover (get_provers whyconf)

exception ProverNotFound of config * string

let prover_by_id whyconf id =
  let potentials =
511
    Mprover.filter (fun _ p -> p.id = id) whyconf.provers in
512 513 514
  match Mprover.keys potentials with
    | [] -> raise (ProverNotFound(whyconf,id))
    | [_] -> snd (Mprover.choose potentials)
515
    |  _  -> assert false (** by the verification done by set_provers *)
516 517 518 519 520 521 522 523 524 525

let () = Exn_printer.register
  (fun fmt exn ->
    match exn with
      | ProverNotFound (config,s) ->
        fprintf fmt "Prover '%s' not found in %s@."
          s (get_conf_file config)
      | e -> raise e
  )

526 527
let get_editors c = c.editors

528 529
let editor_by_id whyconf id =
  Meditor.find id whyconf.editors
530 531 532

(******)

533 534
let get_section config name = assert (name <> "main");
  get_section config.config name
535

536 537
let get_family config name = assert (name <> "prover");
  get_family config.config name
538 539


540 541
let set_section config name section = assert (name <> "main");
  {config with config = set_section config.config name section}
542

543 544
let set_family config name section = assert (name <> "prover");
  {config with config = set_family config.config name section}
545