driver.ml 16.1 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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 Wstdlib
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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
21
open Driver_ast
22
open Call_provers
23

24 25 26 27
let driver_debug =
  Debug.register_flag "interm_task"
    ~desc:"Print intermediate task generated during processing of a driver"

28
(** drivers *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
29

30
type driver = {
31 32 33 34 35 36
  drv_env         : Env.env;
  drv_printer     : string option;
  drv_filename    : string option;
  drv_transform   : string list;
  drv_prelude     : prelude;
  drv_thprelude   : prelude_map;
37
  drv_thuse       : (theory * theory) Mid.t;
38
  drv_blacklist   : string list;
39
  drv_meta        : (theory * Stdecl.t) Mid.t;
40
  drv_res_parser  : prover_result_parser;
Clément Fumex's avatar
Clément Fumex committed
41
  drv_tag         : int;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
42
}
43

44 45
(** parse a driver file *)

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

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

68 69 70 71
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)
72 73
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
74

75
let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files ->
76 77 78 79 80
  let prelude   = ref [] in
  let regexps   = ref [] in
  let exitcodes = ref [] in
  let filename  = ref None in
  let printer   = ref None in
81
  let model_parser = ref "no_model" in
82
  let transform = ref [] in
83
  let timeregexps = ref [] in
84
  let stepregexps = ref [] in
85
  let blacklist = Queue.create () in
86

87
  let set_or_raise loc r v error = match !r with
88
    | Some _ -> raise (Loc.Located (loc, Duplicate error))
89 90 91
    | None   -> r := Some v
  in
  let add_to_list r v = (r := v :: !r) in
92
  let add_global (loc, g) = match g with
93
    | Prelude s -> add_to_list prelude s
94 95 96 97
    | RegexpValid s -> add_to_list regexps (s, Valid)
    | RegexpInvalid s -> add_to_list regexps (s, Invalid)
    | RegexpTimeout s -> add_to_list regexps (s, Timeout)
    | RegexpOutOfMemory s -> add_to_list regexps (s, OutOfMemory)
98
    | RegexpStepLimitExceeded s ->
99
      add_to_list regexps (s, StepLimitExceeded)
100
    | RegexpUnknown (s,t) -> add_to_list regexps (s, Unknown t)
101
    | RegexpFailure (s,t) -> add_to_list regexps (s, Failure t)
102
    | TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
103
    | StepRegexp (r,ns) ->
104
      add_to_list stepregexps (Call_provers.stepregexp r ns)
105 106 107
    | ExitCodeValid s -> add_to_list exitcodes (s, Valid)
    | ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
    | ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)
108 109
    | ExitCodeStepLimitExceeded s ->
      add_to_list exitcodes (s, StepLimitExceeded)
110
    | ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown t)
111
    | ExitCodeFailure (s,t) -> add_to_list exitcodes (s, Failure t)
112
    | Filename s -> set_or_raise loc filename s "filename"
113
    | Printer s -> set_or_raise loc printer s "printer"
114
    | ModelParser s -> model_parser := s
115
    | Transform s -> add_to_list transform s
116
    | Plugin files -> load_plugin (Filename.dirname file) files
117
    | Blacklist sl -> List.iter (fun s -> Queue.add s blacklist) sl
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
118
  in
119
  let f = load_file file in
120 121
  List.iter add_global f.f_global;

Clément Fumex's avatar
Clément Fumex committed
122 123 124
  let thprelude     = ref Mid.empty in
  let meta          = ref Mid.empty in
  let qualid        = ref [] in
125
  let thuse         = ref Mid.empty in
126

127 128
  let find_pr th (loc,q) = try ns_find_pr th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q)))
129
  in
130 131
  let find_ls th (loc,q) = try ns_find_ls th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownLogic (!qualid,q)))
132
  in
133 134
  let find_ts th (loc,q) = try ns_find_ts th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownType (!qualid,q)))
135
  in
136 137 138 139 140 141
  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
142
  let add_meta th td m =
143 144
    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
145
  in
146 147
  (* th_uc is the theory built with the uses forced by the driver *)
  let add_local th th_uc = function
148
    | Rprelude s ->
149
        let l = Mid.find_def [] th.th_name !thprelude in
150 151
        thprelude := Mid.add th.th_name (s::l) !thprelude;
        th_uc
152 153
    | Rsyntaxts (q,s,b) ->
        let td = syntax_type (find_ts th q) s b in
154 155
        add_meta th td meta;
        th_uc
156 157
    | Rsyntaxfs (q,s,b) ->
        let td = syntax_logic (find_fs th q) s b in
158 159
        add_meta th td meta;
        th_uc
160 161
    | Rsyntaxps (q,s,b) ->
        let td = syntax_logic (find_ps th q) s b in
162 163
        add_meta th td meta;
        th_uc
164
    | Rremovepr (q) ->
165
        let td = remove_prop (find_pr th q) in
166 167
        add_meta th td meta;
        th_uc
168 169 170 171 172
    | Rremoveall ->
      let it key _ = match (Mid.find key th.th_known).d_node with
        | Dprop (_,symb,_) -> add_meta th (remove_prop symb) meta
        | _ -> ()
      in
173 174
      Mid.iter it th.th_local;
      th_uc
175 176
    | Rconverter (q,s,b) ->
        let cs = syntax_converter (find_ls th q) s b in
177 178
        add_meta th cs meta;
        th_uc
Clément Fumex's avatar
Clément Fumex committed
179 180
    | Rliteral (q,s,b) ->
        let cs = syntax_literal (find_ts th q) s b in
181 182
        add_meta th cs meta;
        th_uc
183
    | Rmeta (s,al) ->
184 185
        let rec ty_of_pty = function
          | PTyvar x ->
186
              Ty.ty_var (Ty.tv_of_string x)
187 188 189
          | PTyapp ((loc,_) as q,tyl) ->
              let ts = find_ts th q in
              let tyl = List.map ty_of_pty tyl in
190
              Loc.try2 ~loc Ty.ty_app ts tyl
191 192 193 194
          | PTuple tyl ->
              let ts = Ty.ts_tuple (List.length tyl) in
              Ty.ty_app ts (List.map ty_of_pty tyl)
        in
195
        let convert = function
196 197
          | PMAty (PTyapp (q,[]))
                     -> MAts (find_ts th q)
198
          | PMAty ty -> MAty (ty_of_pty ty)
199 200
          | PMAfs q  -> MAls (find_fs th q)
          | PMAps q  -> MAls (find_ps th q)
201 202 203 204
          | PMApr q  -> MApr (find_pr th q)
          | PMAstr s -> MAstr s
          | PMAint i -> MAint i
        in
205 206
        let m = lookup_meta s in
        let td = create_meta m (List.map convert al) in
207 208 209 210 211 212
        add_meta th td meta;
        th_uc
    | Ruse (loc,q) ->
      let file, th = Lists.chop_last q in
      let th = Loc.try3 ~loc Env.read_theory env file th in
      Theory.use_export th_uc th
213
  in
214
  let add_local th th_uc (loc,rule) = Loc.try2 ~loc add_local th th_uc rule in
215
  let add_theory { thr_name = (loc,q); thr_rules = trl } =
216
    let f,id = Lists.chop_last q in
Andrei Paskevich's avatar
Andrei Paskevich committed
217
    let th = Loc.try3 ~loc Env.read_theory env f id in
218
    let th_uc = Theory.create_theory (Ident.id_fresh ~loc ("driver export for "^th.th_name.id_string)) in
219
    qualid := q;
220 221 222
    let th_uc' = List.fold_left (add_local th) th_uc trl in
    if th_uc != th_uc' then
      thuse := Mid.add th.th_name (th, Theory.close_theory th_uc') !thuse
223 224
  in
  List.iter add_theory f.f_rules;
225
  List.iter (fun f -> List.iter add_theory (load_file f).f_rules) extra_files;
226
  incr driver_tag;
227
  {
228 229
    drv_env         = env;
    drv_printer     = !printer;
230
    drv_prelude     = List.rev !prelude;
231
    drv_filename    = !filename;
232 233
    drv_transform   = List.rev !transform;
    drv_thprelude   = Mid.map List.rev !thprelude;
234
    drv_blacklist   = Queue.fold (fun l s -> s :: l) [] blacklist;
235
    drv_meta        = !meta;
Clément Fumex's avatar
Clément Fumex committed
236
    drv_res_parser =
237 238 239
      {
      prp_regexps     = List.rev !regexps;
      prp_timeregexps = List.rev !timeregexps;
240
      prp_stepregexps = List.rev !stepregexps;
241
      prp_exitcodes   = List.rev !exitcodes;
242
      prp_model_parser = Model_parser.lookup_model_parser !model_parser
243
    };
Clément Fumex's avatar
Clément Fumex committed
244
    drv_tag         = !driver_tag;
245
    drv_thuse       = !thuse;
246
  }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
247

248 249 250 251
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

252
(** apply drivers *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
253

254
exception UnknownSpec of string
255

256 257 258
let filename_regexp = Str.regexp "%\\(.\\)"

let get_filename drv input_file theory_name goal_name =
259 260
  let sanitize = Ident.sanitizer
    Ident.char_to_alnumus Ident.char_to_alnumus in
261 262 263 264
  let file = match drv.drv_filename with
    | Some f -> f
    | None -> "%f-%t-%g.dump"
  in
265
  let replace s = match Str.matched_group 1 s with
266
    | "%" -> "%"
267 268 269
    | "f" -> sanitize input_file
    | "t" -> sanitize theory_name
    | "g" -> sanitize goal_name
270
    | s   -> raise (UnknownSpec s)
271
  in
272
  Str.global_substitute filename_regexp replace file
273

274
let file_of_task drv input_file theory_name task =
275
  get_filename drv input_file theory_name (task_goal task).pr_name.id_string
276

277 278 279
let file_of_theory drv input_file th =
  get_filename drv input_file th.th_name.Ident.id_string "null"

280 281
let call_on_buffer ~command ~limit ~gen_new_file ?inplace ~filename
    ~printer_mapping drv buffer =
282
  Call_provers.call_on_buffer
283
    ~command ~limit ~gen_new_file ~res_parser:drv.drv_res_parser
284
    ~filename ~printer_mapping ?inplace buffer
285

286 287 288 289
(** print'n'prove *)

exception NoPrinter

290
let update_task = let ht = Hint.create 5 in fun drv ->
291
    let update task0 =
292
      (** add requested theorie *)
293
      let task0 = Mid.fold (fun _ (th,th') task ->
294 295 296 297 298 299 300 301
          let tdcs = (Task.find_clone_tds task0 th).tds_set in
          Stdecl.fold (fun tdc task -> match tdc.td_node with
              | Use _ -> Task.use_export task th'
              | Clone (_,_) ->
                  (** We do nothing in case of clone *)
                  task
              | _ -> assert false
            ) tdcs task
302 303 304
        ) drv.drv_thuse task0
      in
      (** apply metas *)
305 306 307 308 309 310 311 312 313 314 315
      let task0 = Mid.fold (fun _ (th,tdms) task ->
          let tdcs = (Task.find_clone_tds task0 th).tds_set in
          Stdecl.fold (fun tdc task ->
              Stdecl.fold (fun tdm task -> match tdc.td_node with
                  | Use _ -> add_tdecl task tdm
                  | Clone (_,sm) ->
                      let tdm = Theory.clone_meta tdm th sm in
                      Opt.fold add_tdecl task tdm
                  | _ -> assert false
                ) tdms task
            ) tdcs task
316
        ) drv.drv_meta task0
317 318
      in
      task0
319
    in
320 321 322 323 324 325 326 327 328
  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
329
    | task -> update task
330

331
(* Apply driver's transformations to the task *)
332
let prepare_task drv task =
333
  let lookup_transform t = lookup_transform t drv.drv_env, t in
334
  let transl = List.map lookup_transform drv.drv_transform in
335 336 337 338 339 340 341 342
  let apply task (tr,name) =
    let task = Trans.apply tr task in
    Debug.dprintf driver_debug "Task after transformation: %s\n%a@."
      name Pretty.print_task task;
    task
  in
  Debug.dprintf driver_debug "Task before driver's transformation\n%a@."
    Pretty.print_task task;
343
  let task = update_task drv task in
344 345
  Debug.dprintf driver_debug "Task after update\n%a@."
    Pretty.print_task task;
Andrei Paskevich's avatar
Andrei Paskevich committed
346
  List.fold_left apply task transl
347

348
let print_task_prepared ?old drv fmt task =
349 350 351 352
  let p = match drv.drv_printer with
    | None -> raise NoPrinter
    | Some p -> p
  in
353
  let printer_args = { Printer.env = drv.drv_env;
354 355
      prelude     = drv.drv_prelude;
      th_prelude  = drv.drv_thprelude;
356 357 358 359 360 361
      blacklist   = drv.drv_blacklist;
      printer_mapping = get_default_printer_mapping;
    } in
  let printer = lookup_printer p printer_args in
  fprintf fmt "@[%a@]@?" (printer ?old) task;
  printer_args.printer_mapping
362

363 364
let print_task ?old drv fmt task =
  let task = prepare_task drv task in
365
  let _ = print_task_prepared ?old drv fmt task in
366
  ()
367

368 369
let print_theory ?old drv fmt th =
  let task = Task.use_export None th in
370
  print_task ?old drv fmt task
371

372
let file_name_of_task ?old ?inplace ?interactive drv task =
373
  match old, inplace with
374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395
    | Some fn, Some true ->
        (* Example: Isabelle. No file should be generated, it should be done
           in_place and we keep the same file. *)
        false, fn
    | Some fn, _ when interactive <> Some true ->
        (* Example: cvc4. If a file is provided, it means it was passed to
           schedule_proof_attempt via its save_to argument. So we ask to erase
           and regenerate the file (the advantage is that we decide the location
           of the file).
        *)
        false, fn
    | Some _, _ ->
        (* Example: Coq.
           For Coq, the interactively edited file should be kept (not erased)
           and a new temp file is generated using the old one.
        *)
        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
        true, get_filename drv fn "T" pr.pr_name.id_string
396
    | _ ->
397 398 399
        (* Example: cvc4 without ?save_to argument
           No file were provided. We have to generate a new one.
        *)
400 401 402 403 404
        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
405
        true, get_filename drv fn "T" pr.pr_name.id_string
406

407
let prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task =
408 409
  let buf = Buffer.create 1024 in
  let fmt = formatter_of_buffer buf in
410 411
  let gen_new_file, filename =
    file_name_of_task ?old ?inplace ?interactive drv task in
412 413 414 415
  let old_channel = Opt.map open_in old in
  let printer_mapping = print_task_prepared ?old:old_channel drv fmt task in
  pp_print_flush fmt ();
  Opt.iter close_in old_channel;
416
  let res =
417
    call_on_buffer ~command ~limit ~gen_new_file
418
                   ?inplace ~filename ~printer_mapping drv buf in
419 420
  Buffer.reset buf;
  res
421

422 423
let prove_task ~command ~limit ?old ?inplace ?interactive drv task =
  let task = prepare_task drv task in
424
  prove_task_prepared ~command ~limit ?interactive ?old ?inplace drv task
425

426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443
(* 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
444 445 446 447
  | 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
448
  | e -> raise e)