driver.ml 12.1 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Format
13
open Stdlib
Andrei Paskevich's avatar
Andrei Paskevich committed
14
open Ident
15
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
16
open Decl
17
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
18
open Task
19 20
open Printer
open Trans
21
open Driver_ast
22
open Call_provers
23

24
(** drivers *)
25

26
type driver = {
27 28 29 30 31 32
  drv_env         : Env.env;
  drv_printer     : string option;
  drv_filename    : string option;
  drv_transform   : string list;
  drv_prelude     : prelude;
  drv_thprelude   : prelude_map;
33
  drv_blacklist   : string list;
34 35
  drv_meta        : (theory * Stdecl.t) Mid.t;
  drv_regexps     : (Str.regexp * prover_answer) list;
36
  drv_timeregexps : Call_provers.timeregexp list;
37
  drv_exitcodes   : (int * prover_answer) list;
38
  drv_tag         : int
39
}
40

41 42
(** parse a driver file *)

43
let load_plugin dir (byte,nat) =
Andrei Paskevich's avatar
Andrei Paskevich committed
44
  let file = if Dynlink.is_native then nat else byte in
45
  let file = Filename.concat dir file in
Andrei Paskevich's avatar
Andrei Paskevich committed
46
  Dynlink.loadfile_private file
47

48
let load_file file =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
49 50 51
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
52 53
  let to_close = Stack.create () in
  Stack.push c to_close;
54
  let input_lexer filename =
55 56 57 58 59 60 61 62
    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;
63
  f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
64

65 66 67 68
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)
69 70
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
71

72
let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
73 74 75 76 77
  let prelude   = ref [] in
  let regexps   = ref [] in
  let exitcodes = ref [] in
  let filename  = ref None in
  let printer   = ref None in
78
  let transform = ref [] in
79
  let timeregexps = ref [] in
80
  let blacklist = Queue.create () in
81

82
  let set_or_raise loc r v error = match !r with
83
    | Some _ -> raise (Loc.Located (loc, Duplicate error))
84 85 86
    | None   -> r := Some v
  in
  let add_to_list r v = (r := v :: !r) in
87
  let add_global (loc, g) = match g with
88 89 90 91
    | 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)
92
    | RegexpOutOfMemory s -> add_to_list regexps (Str.regexp s, OutOfMemory)
93 94
    | RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown t)
    | RegexpFailure (s,t) -> add_to_list regexps (Str.regexp s, Failure t)
95
    | TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
96 97 98
    | ExitCodeValid s -> add_to_list exitcodes (s, Valid)
    | ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
    | ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)
99
    | ExitCodeOutOfMemory s -> add_to_list exitcodes (s, OutOfMemory)
100 101
    | ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown t)
    | ExitCodeFailure (s,t) -> add_to_list exitcodes (s, Failure t)
102
    | Filename s -> set_or_raise loc filename s "filename"
103 104
    | Printer s -> set_or_raise loc printer s "printer"
    | Transform s -> add_to_list transform s
105
    | Plugin files -> load_plugin (Filename.dirname file) files
106
    | Blacklist sl -> List.iter (fun s -> Queue.add s blacklist) sl
107
  in
108
  let f = load_file file in
109 110 111
  List.iter add_global f.f_global;

  let thprelude = ref Mid.empty in
112
  let meta      = ref Mid.empty in
113 114
  let qualid    = ref [] in

115 116
  let find_pr th (loc,q) = try ns_find_pr th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q)))
117
  in
118 119
  let find_ls th (loc,q) = try ns_find_ls th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownLogic (!qualid,q)))
120
  in
121 122
  let find_ts th (loc,q) = try ns_find_ts th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownType (!qualid,q)))
123
  in
124 125 126 127 128 129
  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
130
  let add_meta th td m =
131 132
    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
133
  in
134
  let add_local th = function
135
    | Rprelude s ->
136
        let l = Mid.find_def [] th.th_name !thprelude in
137
        thprelude := Mid.add th.th_name (s::l) !thprelude
138
    | Rsyntaxts (q,s) ->
139
        let td = syntax_type (find_ts th q) s in
140 141
        add_meta th td meta
    | Rsyntaxfs (q,s) ->
142
        let td = syntax_logic (find_fs th q) s in
143 144
        add_meta th td meta
    | Rsyntaxps (q,s) ->
145
        let td = syntax_logic (find_ps th q) s in
146 147
        add_meta th td meta
    | Rremovepr (q) ->
148
        let td = remove_prop (find_pr th q) in
149 150
        add_meta th td meta
    | Rmeta (s,al) ->
151 152
        let rec ty_of_pty = function
          | PTyvar x ->
153
              Ty.ty_var (Ty.tv_of_string x)
154 155 156
          | PTyapp ((loc,_) as q,tyl) ->
              let ts = find_ts th q in
              let tyl = List.map ty_of_pty tyl in
157
              Loc.try2 ~loc Ty.ty_app ts tyl
158 159 160 161
          | PTuple tyl ->
              let ts = Ty.ts_tuple (List.length tyl) in
              Ty.ty_app ts (List.map ty_of_pty tyl)
        in
162
        let convert = function
163 164
          | PMAty (PTyapp (q,[]))
                     -> MAts (find_ts th q)
165
          | PMAty ty -> MAty (ty_of_pty ty)
166 167
          | PMAfs q  -> MAls (find_fs th q)
          | PMAps q  -> MAls (find_ps th q)
168 169 170 171
          | PMApr q  -> MApr (find_pr th q)
          | PMAstr s -> MAstr s
          | PMAint i -> MAint i
        in
172 173
        let m = lookup_meta s in
        let td = create_meta m (List.map convert al) in
174
        add_meta th td meta
175
  in
176 177
  let add_local th (loc,rule) =
    try add_local th rule with e -> raise (Loc.Located (loc,e))
178 179 180
  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
181
    let th =
182
      try Env.read_theory env f id
183
      with e when not (Debug.test_flag Debug.stack_trace) ->
184
        raise (Loc.Located (loc,e))
185 186 187 188 189
    in
    qualid := q;
    List.iter (add_local th) trl
  in
  List.iter add_theory f.f_rules;
190
  List.iter (fun f -> List.iter add_theory (load_file f).f_rules) extra_files;
191
  incr driver_tag;
192
  {
193 194
    drv_env         = env;
    drv_printer     = !printer;
195
    drv_prelude     = List.rev !prelude;
196
    drv_filename    = !filename;
197 198
    drv_transform   = List.rev !transform;
    drv_thprelude   = Mid.map List.rev !thprelude;
199
    drv_blacklist   = Queue.fold (fun l s -> s :: l) [] blacklist;
200 201
    drv_meta        = !meta;
    drv_regexps     = List.rev !regexps;
202
    drv_timeregexps = List.rev !timeregexps;
203
    drv_exitcodes   = List.rev !exitcodes;
204
    drv_tag         = !driver_tag
205
  }
206

207 208 209 210
let syntax_map drv =
  let addth _ (_,tds) acc = Stdecl.fold Printer.add_syntax_map tds acc in
  Mid.fold addth drv.drv_meta Mid.empty

211
(** apply drivers *)
212

213
exception UnknownSpec of string
214

215 216 217
let filename_regexp = Str.regexp "%\\(.\\)"

let get_filename drv input_file theory_name goal_name =
218 219
  let sanitize = Ident.sanitizer
    Ident.char_to_alnumus Ident.char_to_alnumus in
220 221 222 223
  let file = match drv.drv_filename with
    | Some f -> f
    | None -> "%f-%t-%g.dump"
  in
224
  let replace s = match Str.matched_group 1 s with
225
    | "%" -> "%"
226 227 228
    | "f" -> sanitize input_file
    | "t" -> sanitize theory_name
    | "g" -> sanitize goal_name
229
    | s   -> raise (UnknownSpec s)
230
  in
231
  Str.global_substitute filename_regexp replace file
232

233
let file_of_task drv input_file theory_name task =
234
  get_filename drv input_file theory_name (task_goal task).pr_name.id_string
235

236 237 238
let file_of_theory drv input_file th =
  get_filename drv input_file th.th_name.Ident.id_string "null"

239
let call_on_buffer ~command ?timelimit ?memlimit ?inplace ~filename drv buffer =
240
  let regexps = drv.drv_regexps in
241
  let timeregexps = drv.drv_timeregexps in
242 243
  let exitcodes = drv.drv_exitcodes in
  Call_provers.call_on_buffer
244
    ~command ?timelimit ?memlimit ~regexps ~timeregexps
245
    ~exitcodes ~filename ?inplace buffer
246

247 248 249 250
(** print'n'prove *)

exception NoPrinter

251 252
let update_task = let ht = Hint.create 5 in fun drv ->
  let update task0 =
253
    Mid.fold (fun _ (th,s) task ->
254
      Task.on_theory th (fun task sm ->
255
        Stdecl.fold (fun tdm task ->
256
          add_tdecl task (clone_meta tdm sm)
257
        ) s task
258 259
      ) task task0
    ) drv.drv_meta task0
260
  in
261 262 263 264 265 266 267 268 269 270
  function
  | Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,_)}} as goal;
          task_prev = task} ->
      (* we cannot add metas nor memoize after goal *)
      let update = try Hint.find ht drv.drv_tag with Not_found ->
        let upd = Trans.store update in
        Hint.add ht drv.drv_tag upd; upd in
      let task = Trans.apply update task in
      add_tdecl task goal
  | task -> update task
271

272
let prepare_task drv task =
273
  let lookup_transform t = lookup_transform t drv.drv_env in
274
  let transl = List.map lookup_transform drv.drv_transform in
275
  let apply task tr = Trans.apply tr task in
276
  let task = update_task drv task in
277
  List.fold_left apply task transl
278

279
let print_task_prepared ?old drv fmt task =
280 281 282 283
  let p = match drv.drv_printer with
    | None -> raise NoPrinter
    | Some p -> p
  in
284 285 286 287 288
  let printer = lookup_printer p
    { Printer.env = drv.drv_env;
      prelude     = drv.drv_prelude;
      th_prelude  = drv.drv_thprelude;
      blacklist   = drv.drv_blacklist } in
289
  fprintf fmt "@[%a@]@?" (printer ?old) task
290

291
let print_task ?old drv fmt task =
292
  let task = prepare_task drv task in
293
  print_task_prepared ?old drv fmt task
294

295 296
let print_theory ?old drv fmt th =
  let task = Task.use_export None th in
297
  print_task ?old drv fmt task
298

299 300
let prove_task_prepared
  ~command ?timelimit ?memlimit ?old ?inplace drv task =
301 302
  let buf = Buffer.create 1024 in
  let fmt = formatter_of_buffer buf in
303
  let old_channel = Opt.map open_in old in
304
  print_task_prepared ?old:old_channel drv fmt task; pp_print_flush fmt ();
305
  Opt.iter close_in old_channel;
306 307 308 309 310 311 312 313 314
  let filename = match old, inplace with
    | Some fn, Some true -> fn
    | _ ->
        let pr = Task.task_goal task in
        let fn = match pr.pr_name.id_loc with
          | Some loc -> let fn,_,_,_ = Loc.get loc in Filename.basename fn
          | None -> "" in
        let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
        get_filename drv fn "T" pr.pr_name.id_string
315
  in
316 317
  let res =
    call_on_buffer ~command ?timelimit ?memlimit ?inplace ~filename drv buf in
318 319
  Buffer.reset buf;
  res
320

321
let prove_task ~command ?timelimit ?memlimit ?old ?inplace drv task =
322
  let task = prepare_task drv task in
323
  prove_task_prepared ~command ?timelimit ?memlimit ?old ?inplace drv task
324

325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342
(* 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
343 344 345 346
  | 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
347 348
  | e -> raise e)