whyconf.ml 11.3 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
(*    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
19 20

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

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

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

39
let magicnumber = 11
40

41 42
exception WrongMagicNumber

43 44
(* lib and shared dirs *)

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

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

54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
(* Prover *)

type prover =
    { prover_id : string;
      prover_name : string;
      prover_version : string;
    }

let print_prover fmt p =
  Format.fprintf fmt "%s(%s)" p.prover_name p.prover_version

module Prover = struct
  type t = prover
  let compare s1 s2 =
    if s1 == s2 then 0 else
    let c = String.compare s1.prover_id s2.prover_id in
    if c <> 0 then c 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
    c

  let equal s1 s2 =
    s1.prover_id = s2.prover_id &&
      s1.prover_name = s2.prover_name &&
      s1.prover_version = s2.prover_version

  let hash s1 =
    2 * Hashtbl.hash s1.prover_id +
      3 * Hashtbl.hash s1.prover_name +
      5 * Hashtbl.hash s1.prover_version


end

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

93 94 95
(* Configuration file *)

type config_prover = {
96 97 98
  name    : string;   (* "Alt-Ergo v2.95 (special)" *)
  command : string;   (* "exec why-limit %t %m alt-ergo %f" *)
  driver  : string;   (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
99 100
  version : string;   (* "v2.95" *)
  editor  : string;
101
  interactive : bool;
102 103 104
}

type main = {
105 106
  libdir   : string;      (* "/usr/local/lib/why/" *)
  datadir  : string;      (* "/usr/local/share/why/" *)
107
  loadpath  : string list;  (* "/usr/local/lib/why/theories" *)
108 109
  timelimit : int;
  (* default prover time limit in seconds (0 unlimited) *)
110
  memlimit  : int;
111
  (* default prover memory limit in megabytes (0 unlimited)*)
112
  running_provers_max : int;
113
  (* max number of running prover processes *)
François Bobot's avatar
François Bobot committed
114
  plugins : string list;
115
  (* plugins to load, without extension, relative to [libdir]/plugins *)
116 117
}

MARCHE Claude's avatar
MARCHE Claude committed
118 119 120
let libdir m =
  try
    Sys.getenv "WHY3LIB"
121
  with Not_found -> m.libdir
MARCHE Claude's avatar
MARCHE Claude committed
122 123 124

let datadir m =
  try
125 126 127 128 129
    let d = Sys.getenv "WHY3DATA" in
(*
    eprintf "[Info] datadir set using WHY3DATA='%s'@." d;
*)
    d
130
  with Not_found -> m.datadir
MARCHE Claude's avatar
MARCHE Claude committed
131

132
let loadpath m =
133 134 135 136 137
  try
    let d = Sys.getenv "WHY3LOADPATH" in
(*
    eprintf "[Info] loadpath set using WHY3LOADPATH='%s'@." d;
*)
138
    Str.split (Str.regexp ":") d
139 140 141 142 143 144 145 146 147
  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
148 149 150 151
let plugins m = m.plugins
let set_plugins m pl =
  (* TODO : sanitize? *)
  { m with plugins = pl}
152

François Bobot's avatar
François Bobot committed
153 154 155 156 157
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
158
let pluginsdir m = Filename.concat m.libdir "plugins"
François Bobot's avatar
François Bobot committed
159 160
let load_plugins m =
  let load x =
161
    try Plugin.load x
162 163 164
    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
165 166
  List.iter load m.plugins

167
type config = {
168
  conf_file : string;       (* "/home/innocent_user/.why3.conf" *)
169
  config    : Rc.t;
170
  main      : main;
171
  provers   : config_prover Mprover.t;
172 173
}

174 175
let default_main =
  {
176 177 178
    libdir = Config.libdir;
    datadir = Config.datadir;
    loadpath = default_loadpath;
179 180 181
    timelimit = 10;
    memlimit = 0;
    running_provers_max = 2;
François Bobot's avatar
François Bobot committed
182
    plugins = [];
183
  }
184

185
let set_main rc main =
186
  let section = empty_section in
187
  let section = set_int section "magic" magicnumber in
188 189 190 191 192
  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
193 194 195 196
  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
197
  let section = set_stringl section "plugin" main.plugins in
198
  set_section rc "main" section
199

200
let set_prover prover_id prover family =
201 202 203 204 205 206
  let section = empty_section in
  let section = set_string section "name" prover.name in
  let section = set_string section "command" prover.command in
  let section = set_string section "driver" prover.driver in
  let section = set_string section "version" prover.version in
  let section = set_string section "editor" prover.editor in
207
  let section = set_bool section "interactive" prover.interactive in
208
  (prover_id.prover_id,section)::family
209

210
let set_provers rc provers =
211
  let family = Mprover.fold set_prover provers [] in
212
  set_family rc "prover" family
213

214
let absolute_filename = Sysutil.absolutize_filename
215

216
let load_prover dirname provers (id,section) =
217 218 219 220 221 222 223 224 225
  let version = get_string ~default:"" section "version" in
  let name = get_string section "name" in
  let prover =
    { prover_id = id;
      prover_name = name;
      prover_version = version }
  in
  Mprover.add prover
    { name    = name;
226 227
      command = get_string section "command";
      driver  = absolute_filename dirname (get_string section "driver");
228
      version = version;
229
      editor  = get_string ~default:"" section "editor";
230
      interactive = get_bool ~default:false section "interactive";
231 232 233
    } provers

let load_main dirname section =
234 235
  if get_int ~default:0 section "magic" <> magicnumber then
    raise WrongMagicNumber;
236 237
  { libdir    = get_string ~default:default_main.libdir section "libdir";
    datadir   = get_string ~default:default_main.datadir section "datadir";
238
    loadpath  = List.map (absolute_filename dirname)
239
      (get_stringl ~default:[] section "loadpath");
240 241
    timelimit = get_int ~default:default_main.timelimit section "timelimit";
    memlimit  = get_int ~default:default_main.memlimit section "memlimit";
242 243
    running_provers_max = get_int ~default:default_main.running_provers_max
      section "running_provers_max";
François Bobot's avatar
François Bobot committed
244
    plugins = get_stringl ~default:[] section "plugin";
245 246
  }

247
let read_config_rc conf_file =
248 249
  let filename = match conf_file with
    | Some filename -> filename
250
    | None -> begin try Sys.getenv "WHY3CONFIG" with Not_found ->
251 252
          if Sys.file_exists default_conf_file then default_conf_file
          else raise Exit
253 254
        end
  in
255 256 257 258 259
  filename, Rc.from_file filename

exception ConfigFailure of string (* filename *) * string

let () = Exn_printer.register (fun fmt e -> match e with
260
  | ConfigFailure (f, s) ->
261
      Format.fprintf fmt "error in config file %s: %s" f s
262 263
  | WrongMagicNumber ->
      Format.fprintf fmt "outdated config file; rerun why3config"
264
  | _ -> raise e)
265 266 267 268 269

let get_config (filename,rc) =
  let dirname = Filename.dirname filename in
  let rc, main =
    match get_section rc "main" with
270
      | None      -> raise (ConfigFailure (filename, "no main section"))
271
      | Some main -> rc, load_main dirname main
272
  in
273
  let provers = get_family rc "prover" in
274
  let provers = List.fold_left (load_prover dirname) Mprover.empty provers in
275
  { conf_file = filename;
276 277 278
    config    = rc;
    main      = main;
    provers   = provers;
279
  }
280

281
let default_config conf_file =
282
  get_config (conf_file, set_main Rc.empty default_main)
283

284
let read_config conf_file =
285 286
  let filenamerc =
    try
287
      read_config_rc conf_file
288
    with Exit ->
289 290
      default_conf_file, set_main Rc.empty default_main
  in
291
  try
292
    get_config filenamerc
293 294 295 296
  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))
297

298
let save_config config =
299
  let filename = config.conf_file in
300
  Sysutil.backup_file filename;
301
  to_file filename config.config
302

303 304
let get_main config = config.main
let get_provers config = config.provers
305

306 307 308 309
let set_main config main =
  {config with
    config = set_main config.config main;
    main = main;
310 311
  }

312 313 314 315 316
let set_provers config provers =
  {config with
    config = set_provers config.config provers;
    provers = provers;
  }
317

318 319
(*******)

320
let set_conf_file config conf_file = {config with conf_file = conf_file}
321
let get_conf_file config           =  config.conf_file
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 347 348 349 350 351 352 353 354
(*******)

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

exception ProverNotFound of config * string
exception ProverAmbiguity of config * string * prover list

let prover_by_id whyconf id =
  let potentials =
    Mprover.filter (fun p _ -> p.prover_id = id) whyconf.provers in
  match Mprover.keys potentials with
    | [] -> raise (ProverNotFound(whyconf,id))
    | [_] -> snd (Mprover.choose potentials)
    |  l -> raise (ProverAmbiguity(whyconf,id,l))

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)
      | ProverAmbiguity (config,s,l) ->
        fprintf fmt "More than one provers corresponds to '%s' in %s:@.%a@."
          s (get_conf_file config)
          (Pp.print_list Pp.newline print_prover) l
      | e -> raise e
  )


(******)

355 356
let get_section config name = assert (name <> "main");
  get_section config.config name
357

358 359
let get_family config name = assert (name <> "prover");
  get_family config.config name
360 361


362 363
let set_section config name section = assert (name <> "main");
  {config with config = set_section config.config name section}
364

365 366
let set_family config name section = assert (name <> "prover");
  {config with config = set_family config.config name section}
367