driver.ml 11.6 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 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.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Format
Andrei Paskevich's avatar
Andrei Paskevich committed
21 22
open Util
open Ident
23 24
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
25
open Decl
26
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
27
open Task
28 29
open Printer
open Trans
30
open Driver_ast
31
open Call_provers
32

33
(** drivers *)
34

35
type driver = {
36 37 38 39 40 41 42 43 44
  drv_env         : Env.env;
  drv_printer     : string option;
  drv_filename    : string option;
  drv_transform   : string list;
  drv_prelude     : prelude;
  drv_thprelude   : prelude_map;
  drv_meta        : (theory * Stdecl.t) Mid.t;
  drv_meta_cl     : (theory * Stdecl.t) Mid.t;
  drv_regexps     : (Str.regexp * prover_answer) list;
45
  drv_timeregexps : Call_provers.timeregexp list;
46
  drv_exitcodes   : (int * prover_answer) list;
47
  drv_tag         : int
48
}
49

50 51
(** parse a driver file *)

52
let load_plugin dir (byte,nat) =
Andrei Paskevich's avatar
Andrei Paskevich committed
53
  let file = if Dynlink.is_native then nat else byte in
54
  let file = Filename.concat dir file in
Andrei Paskevich's avatar
Andrei Paskevich committed
55
  Dynlink.loadfile_private file
56

57
let load_file file =
58
  let basename = Filename.dirname file in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
59 60 61
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
62 63 64 65 66 67 68 69 70 71 72 73
  let to_close = Stack.create () in
  Stack.push c to_close;
  let input_lexer s =
    let filename = Sysutil.absolutize_filename basename s in
    let c = open_in filename in
    Stack.push c to_close;
    let lb = Lexing.from_channel c in
    Loc.set_file filename lb;
    lb
  in
  let f = Driver_lexer.parse_file input_lexer lb in
  Stack.iter close_in to_close;
74
  f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
75

76 77 78 79
exception Duplicate    of string
exception UnknownType  of (string list * string list)
exception UnknownLogic of (string list * string list)
exception UnknownProp  of (string list * string list)
80 81
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
82

83
let load_driver = let driver_tag = ref (-1) in fun env file ->
84 85 86 87 88
  let prelude   = ref [] in
  let regexps   = ref [] in
  let exitcodes = ref [] in
  let filename  = ref None in
  let printer   = ref None in
89
  let transform = ref [] in
90
  let timeregexps = ref [] in
91

92
  let set_or_raise loc r v error = match !r with
93
    | Some _ -> raise (Loc.Located (loc, Duplicate error))
94 95 96
    | None   -> r := Some v
  in
  let add_to_list r v = (r := v :: !r) in
97
  let add_global (loc, g) = match g with
98 99 100 101 102 103
    | Prelude s -> add_to_list prelude s
    | RegexpValid s -> add_to_list regexps (Str.regexp s, Valid)
    | RegexpInvalid s -> add_to_list regexps (Str.regexp s, Invalid)
    | RegexpTimeout s -> add_to_list regexps (Str.regexp s, Timeout)
    | RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown t)
    | RegexpFailure (s,t) -> add_to_list regexps (Str.regexp s, Failure t)
104
    | TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
105 106 107 108 109
    | ExitCodeValid s -> add_to_list exitcodes (s, Valid)
    | ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
    | ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)
    | ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown t)
    | ExitCodeFailure (s,t) -> add_to_list exitcodes (s, Failure t)
110
    | Filename s -> set_or_raise loc filename s "filename"
111 112
    | Printer s -> set_or_raise loc printer s "printer"
    | Transform s -> add_to_list transform s
113
    | Plugin files -> load_plugin (Filename.dirname file) files
114
  in
115
  let f = load_file file in
116 117 118
  List.iter add_global f.f_global;

  let thprelude = ref Mid.empty in
119 120
  let meta      = ref Mid.empty in
  let meta_cl   = ref Mid.empty in
121 122
  let qualid    = ref [] in

123 124
  let find_pr th (loc,q) = try ns_find_pr th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q)))
125
  in
126 127
  let find_ls th (loc,q) = try ns_find_ls th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownLogic (!qualid,q)))
128
  in
129 130
  let find_ts th (loc,q) = try ns_find_ts th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownType (!qualid,q)))
131
  in
132 133 134 135 136 137
  let find_fs th q =
    let ls = find_ls th q in
    if ls.ls_value = None then raise (FSymExpected ls) else ls in
  let find_ps th q =
    let ls = find_ls th q in
    if ls.ls_value <> None then raise (PSymExpected ls) else ls in
138
  let add_meta th td m =
139 140
    let s = try snd (Mid.find th.th_name !m) with Not_found -> Stdecl.empty in
    m := Mid.add th.th_name (th, Stdecl.add td s) !m
141
  in
142
  let add_local th = function
143
    | Rprelude s ->
144 145
        let l = Mid.find_default th.th_name [] !thprelude in
        thprelude := Mid.add th.th_name (s::l) !thprelude
146 147 148
    | Rsyntaxts (c,q,s) ->
        let td = syntax_type (find_ts th q) s in
        add_meta th td (if c then meta_cl else meta)
149 150 151 152 153
    | Rsyntaxfs (c,q,s) ->
        let td = syntax_logic (find_fs th q) s in
        add_meta th td (if c then meta_cl else meta)
    | Rsyntaxps (c,q,s) ->
        let td = syntax_logic (find_ps th q) s in
154
        add_meta th td (if c then meta_cl else meta)
155
    | Rremovepr (c,q) ->
156 157
        let td = remove_prop (find_pr th q) in
        add_meta th td (if c then meta_cl else meta)
158 159 160
    | Rmeta (c,s,al) ->
        let convert = function
          | PMAts q  -> MAts (find_ts th q)
161 162
          | PMAfs q  -> MAls (find_fs th q)
          | PMAps q  -> MAls (find_ps th q)
163 164 165 166
          | PMApr q  -> MApr (find_pr th q)
          | PMAstr s -> MAstr s
          | PMAint i -> MAint i
        in
167 168
        let m = lookup_meta s in
        let td = create_meta m (List.map convert al) in
169
        add_meta th td (if c then meta_cl else meta)
170
  in
171 172
  let add_local th (loc,rule) =
    try add_local th rule with e -> raise (Loc.Located (loc,e))
173 174 175
  in
  let add_theory { thr_name = (loc,q); thr_rules = trl } =
    let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
176
    let th =
177 178
      try Env.read_theory ~format:"why" env f id
      with e -> raise (Loc.Located (loc,e))
179 180 181 182 183
    in
    qualid := q;
    List.iter (add_local th) trl
  in
  List.iter add_theory f.f_rules;
184
  incr driver_tag;
185
  {
186 187
    drv_env         = env;
    drv_printer     = !printer;
188
    drv_prelude     = List.rev !prelude;
189
    drv_filename    = !filename;
190 191
    drv_transform   = List.rev !transform;
    drv_thprelude   = Mid.map List.rev !thprelude;
192 193 194
    drv_meta        = !meta;
    drv_meta_cl     = !meta_cl;
    drv_regexps     = List.rev !regexps;
195
    drv_timeregexps = List.rev !timeregexps;
196
    drv_exitcodes   = List.rev !exitcodes;
197
    drv_tag         = !driver_tag
198
  }
199

200
(** apply drivers *)
201

202
exception UnknownSpec of string
203

204 205 206
let filename_regexp = Str.regexp "%\\(.\\)"

let get_filename drv input_file theory_name goal_name =
207 208
  let sanitize = Ident.sanitizer
    Ident.char_to_alnumus Ident.char_to_alnumus in
209 210 211 212
  let file = match drv.drv_filename with
    | Some f -> f
    | None -> "%f-%t-%g.dump"
  in
213
  let replace s = match Str.matched_group 1 s with
214
    | "%" -> "%"
215 216 217
    | "f" -> sanitize input_file
    | "t" -> sanitize theory_name
    | "g" -> sanitize goal_name
218
    | s   -> raise (UnknownSpec s)
219
  in
220
  Str.global_substitute filename_regexp replace file
221

222
let file_of_task drv input_file theory_name task =
223
  get_filename drv input_file theory_name (task_goal task).pr_name.id_string
224

225 226 227
let file_of_theory drv input_file th =
  get_filename drv input_file th.th_name.Ident.id_string "null"

228
let call_on_buffer ~command ?timelimit ?memlimit drv buffer =
229
  let regexps = drv.drv_regexps in
230
  let timeregexps = drv.drv_timeregexps in
231 232 233
  let exitcodes = drv.drv_exitcodes in
  let filename = get_filename drv "" "" "" in
  Call_provers.call_on_buffer
234
    ~command ?timelimit ?memlimit ~regexps ~timeregexps
235
    ~exitcodes ~filename buffer
236

237 238 239 240
(** print'n'prove *)

exception NoPrinter

241 242 243 244
let update_task drv task =
  let task, goal = match task with
    | Some { task_decl = g ; task_prev = t } -> t,g
    | None -> raise Task.GoalNotFound
245 246 247
  in
  let task =
    Mid.fold (fun _ (th,s) task ->
248 249 250 251 252
      if Task.on_used_theory th task then
        Stdecl.fold (fun tdm task ->
          add_tdecl task tdm
        ) s task
      else task
253 254 255 256
    ) drv.drv_meta task
  in
  let task =
    Mid.fold (fun _ (th,s) task ->
257
      Task.on_theory th (fun task sm ->
258
        Stdecl.fold (fun tdm task ->
259
          add_tdecl task (clone_meta tdm sm)
260
        ) s task
261
      ) task task
262 263
    ) drv.drv_meta_cl task
  in
264 265
  add_tdecl task goal

266 267 268 269 270 271 272 273 274 275 276
let update_task =
  let h = Hashtbl.create 5 in
  fun drv ->
    let update = try Hashtbl.find h drv.drv_tag with
      | Not_found ->
          let upd = Trans.store (update_task drv) in
          Hashtbl.add h drv.drv_tag upd;
          upd
    in
    Trans.apply update

277
let prepare_task drv task =
278
  let lookup_transform t = lookup_transform t drv.drv_env in
279
  let transl = List.map lookup_transform drv.drv_transform in
280
  let apply task tr = Trans.apply tr task in
281
  let task = update_task drv task in
282
  List.fold_left apply task transl
283

284
let print_task_prepared ?old drv fmt task =
285 286 287 288 289 290 291
  let p = match drv.drv_printer with
    | None -> raise NoPrinter
    | Some p -> p
  in
  let printer =
    lookup_printer p drv.drv_env drv.drv_prelude drv.drv_thprelude
  in
292
  fprintf fmt "@[%a@]@?" (printer ?old) task
293

294
let print_task ?old drv fmt task =
295
  let task = prepare_task drv task in
296
  print_task_prepared ?old drv fmt task
297

298 299
let print_theory ?old drv fmt th =
  let task = Task.use_export None th in
300
  print_task ?old drv fmt task
301

302
let prove_task_prepared ~command ?timelimit ?memlimit ?old drv task =
303 304
  let buf = Buffer.create 1024 in
  let fmt = formatter_of_buffer buf in
305
  print_task_prepared ?old drv fmt task; pp_print_flush fmt ();
306 307 308
  let res = call_on_buffer ~command ?timelimit ?memlimit drv buf in
  Buffer.reset buf;
  res
309

310 311 312 313
let prove_task ~command ?timelimit ?memlimit ?old drv task =
  let task = prepare_task drv task in
  prove_task_prepared ~command ?timelimit ?memlimit ?old drv task

314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331
(* exception report *)

let string_of_qualid thl idl =
  String.concat "." thl ^ "." ^ String.concat "." idl

let () = Exn_printer.register (fun fmt exn -> match exn with
  | NoPrinter -> Format.fprintf fmt
      "No printer specified in the driver file"
  | Duplicate s -> Format.fprintf fmt
      "Duplicate %s specification" s
  | UnknownType (thl,idl) -> Format.fprintf fmt
      "Unknown type symbol %s" (string_of_qualid thl idl)
  | UnknownLogic (thl,idl) -> Format.fprintf fmt
      "Unknown logical symbol %s" (string_of_qualid thl idl)
  | UnknownProp (thl,idl) -> Format.fprintf fmt
      "Unknown proposition %s" (string_of_qualid thl idl)
  | UnknownSpec s -> Format.fprintf fmt
      "Unknown format specifier '%%%s', use %%f, %%t or %%g" s
332 333 334 335
  | FSymExpected ls -> Format.fprintf fmt
      "%a is not a function symbol" Pretty.print_ls ls
  | PSymExpected ls -> Format.fprintf fmt
      "%a is not a predicate symbol" Pretty.print_ls ls
336 337
  | e -> raise e)