driver.ml 13.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   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 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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
21
open Driver_ast
22
open Call_provers
23

24
(** drivers *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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
  drv_meta        : (theory * Stdecl.t) Mid.t;
35
  drv_res_parser  : prover_result_parser;
Clément Fumex's avatar
Clément Fumex committed
36
  drv_tag         : int;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
37
}
38

39 40
(** parse a driver file *)

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

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

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

70
let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
71 72 73 74 75
  let prelude   = ref [] in
  let regexps   = ref [] in
  let exitcodes = ref [] in
  let filename  = ref None in
  let printer   = ref None in
76
  let model_parser = ref "no_model" in
77
  let transform = ref [] in
78
  let timeregexps = ref [] in
79
  let stepregexps = 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
    | RegexpStepLimitExceeded s ->
      add_to_list regexps (Str.regexp s, StepLimitExceeded)
95
    | RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown (t, None))
96
    | RegexpFailure (s,t) -> add_to_list regexps (Str.regexp s, Failure t)
97
    | TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
98
    | StepRegexp (r,ns) ->
99
      add_to_list stepregexps (Call_provers.stepregexp r ns)
100 101 102
    | ExitCodeValid s -> add_to_list exitcodes (s, Valid)
    | ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
    | ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)
103
    | ExitCodeOutOfMemory s -> add_to_list exitcodes (s, OutOfMemory)
104 105
    | ExitCodeStepLimitExceeded s ->
      add_to_list exitcodes (s, StepLimitExceeded)
106
    | ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown (t, None))
107
    | ExitCodeFailure (s,t) -> add_to_list exitcodes (s, Failure t)
108
    | Filename s -> set_or_raise loc filename s "filename"
109
    | Printer s -> set_or_raise loc printer s "printer"
110
    | ModelParser s -> model_parser := s
111
    | Transform s -> add_to_list transform s
112
    | Plugin files -> load_plugin (Filename.dirname file) files
113
    | Blacklist sl -> List.iter (fun s -> Queue.add s blacklist) sl
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114
  in
115
  let f = load_file file in
116 117
  List.iter add_global f.f_global;

Clément Fumex's avatar
Clément Fumex committed
118 119 120
  let thprelude     = ref Mid.empty in
  let meta          = ref Mid.empty in
  let qualid        = ref [] in
121

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

222 223 224 225
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

226
(** apply drivers *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
227

228
exception UnknownSpec of string
229

230 231 232
let filename_regexp = Str.regexp "%\\(.\\)"

let get_filename drv input_file theory_name goal_name =
233 234
  let sanitize = Ident.sanitizer
    Ident.char_to_alnumus Ident.char_to_alnumus in
235 236 237 238
  let file = match drv.drv_filename with
    | Some f -> f
    | None -> "%f-%t-%g.dump"
  in
239
  let replace s = match Str.matched_group 1 s with
240
    | "%" -> "%"
241 242 243
    | "f" -> sanitize input_file
    | "t" -> sanitize theory_name
    | "g" -> sanitize goal_name
244
    | s   -> raise (UnknownSpec s)
245
  in
246
  Str.global_substitute filename_regexp replace file
247

248
let file_of_task drv input_file theory_name task =
249
  get_filename drv input_file theory_name (task_goal task).pr_name.id_string
250

251 252 253
let file_of_theory drv input_file th =
  get_filename drv input_file th.th_name.Ident.id_string "null"

254
let call_on_buffer ~command ~limit
255
                   ?inplace ?interactive ~filename ~printer_mapping drv buffer =
256
  Call_provers.call_on_buffer
257
    ~command ~limit ~res_parser:drv.drv_res_parser
258
    ~filename ~printer_mapping ?inplace ?interactive buffer
259

260

261 262 263 264
(** print'n'prove *)

exception NoPrinter

265 266
let update_task = let ht = Hint.create 5 in fun drv ->
  let update task0 =
267
    Mid.fold (fun _ (th,s) task ->
268
      Task.on_theory th (fun task sm ->
269
        Stdecl.fold (fun tdm task ->
270
          add_tdecl task (clone_meta tdm sm)
271
        ) s task
272 273
      ) task task0
    ) drv.drv_meta task0
274
  in
275 276 277 278 279 280 281 282 283 284
  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
285

286 287 288 289 290 291 292 293 294 295
let add_cntexample_meta task cntexample =
  if not (cntexample) then task
  else
    let cnt_meta = lookup_meta "get_counterexmp" in
    let g,task = Task.task_separate_goal task in
    let task = Task.add_meta task cnt_meta [] in
    Task.add_tdecl task g

let prepare_task ~cntexample drv task =
  let task = add_cntexample_meta task cntexample in
Andrei Paskevich's avatar
Andrei Paskevich committed
296
  let lookup_transform t = lookup_transform t drv.drv_env in
297
  let transl = List.map lookup_transform drv.drv_transform in
Andrei Paskevich's avatar
Andrei Paskevich committed
298
  let apply task tr = Trans.apply tr task in
299
  let task = update_task drv task in
Andrei Paskevich's avatar
Andrei Paskevich committed
300
  List.fold_left apply task transl
301

302
let print_task_prepared ?old drv fmt task =
303 304 305 306
  let p = match drv.drv_printer with
    | None -> raise NoPrinter
    | Some p -> p
  in
307
  let printer_args = { Printer.env = drv.drv_env;
308 309
      prelude     = drv.drv_prelude;
      th_prelude  = drv.drv_thprelude;
310 311 312 313 314 315
      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
316

317
let print_task ?old ?(cntexample=false) drv fmt task =
318
  let task = prepare_task ~cntexample drv task in
319
  let _ = print_task_prepared ?old drv fmt task in
320
  ()
321

322 323
let print_theory ?old drv fmt th =
  let task = Task.use_export None th in
324
  print_task ?old drv fmt task
325

326 327 328 329 330 331 332 333
let prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task =
  let buf = Buffer.create 1024 in
  let fmt = formatter_of_buffer buf in
  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;
  let filename = match old, inplace with
334 335 336 337 338 339 340 341
    | 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
342
  in
343
  let res =
344
    call_on_buffer ~command ~limit
345
                   ?inplace ?interactive ~filename ~printer_mapping drv buf in
346 347
  Buffer.reset buf;
  res
348

349 350
let prove_task ~command ~limit ?(cntexample=false) ?old
               ?inplace ?interactive drv task =
351
  let task = prepare_task ~cntexample drv task in
352
  prove_task_prepared ~command ~limit ?old ?inplace ?interactive drv task
353

354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371
(* 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
372 373 374 375
  | 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
376
  | e -> raise e)