driver.ml 9.73 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
30
open Driver_ast
31
open Call_provers
32

33
(** drivers *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
34

35
type driver = {
36
  drv_env       : Env.env;
37
  drv_printer   : string option;
38
  drv_filename  : string option;
39
  drv_transform : string list;
40 41 42 43 44 45
  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;
  drv_exitcodes : (int * prover_answer) list;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
46
}
47

48 49
(** parse a driver file *)

50 51
exception NoPlugins

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
58
let load_file file =
Jean-Christophe Filliâtre's avatar
drivers  
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
  let f = Driver_lexer.parse_file lb in
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
63
  close_in c;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
64
  f
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
65

66 67 68 69
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)
70

71
let load_driver = let driver_tag = ref (-1) in fun env file ->
72 73 74 75 76
  let prelude   = ref [] in
  let regexps   = ref [] in
  let exitcodes = ref [] in
  let filename  = ref None in
  let printer   = ref None in
77
  let transform = ref [] in
78

79
  let set_or_raise loc r v error = match !r with
80
    | Some _ -> raise (Loc.Located (loc, Duplicate error))
81 82 83
    | None   -> r := Some v
  in
  let add_to_list r v = (r := v :: !r) in
84
  let add_global (loc, g) = match g with
85 86 87 88 89 90 91 92 93 94 95
    | 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)
    | 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)
96
    | Filename s -> set_or_raise loc filename s "filename"
97 98
    | Printer s -> set_or_raise loc printer s "printer"
    | Transform s -> add_to_list transform s
99
    | Plugin files -> load_plugin (Filename.dirname file) files
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
100
  in
101
  let f = load_file file in
102 103 104
  List.iter add_global f.f_global;

  let thprelude = ref Mid.empty in
105 106
  let meta      = ref Mid.empty in
  let meta_cl   = ref Mid.empty in
107 108
  let qualid    = ref [] in

109 110
  let find_pr th (loc,q) = try ns_find_pr th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q)))
111
  in
112 113
  let find_ls th (loc,q) = try ns_find_ls th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownLogic (!qualid,q)))
114
  in
115 116
  let find_ts th (loc,q) = try ns_find_ts th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownType (!qualid,q)))
117
  in
118
  let add_meta th td m =
119 120
    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
121
  in
122
  let add_local th = function
123 124
    | Rprelude s ->
        let l = try Mid.find th.th_name !thprelude with Not_found -> [] in
125
        thprelude := Mid.add th.th_name (l @ [s]) !thprelude
Andrei Paskevich's avatar
Andrei Paskevich committed
126 127 128 129 130 131
    | 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)
    | Rsyntaxls (c,q,s) ->
        let td = syntax_logic (find_ls th q) s in
        add_meta th td (if c then meta_cl else meta)
132
    | Rremovepr (c,q) ->
133 134
        let td = remove_prop (find_pr th q) in
        add_meta th td (if c then meta_cl else meta)
135 136 137 138 139 140 141 142
    | Rmeta (c,s,al) ->
        let convert = function
          | PMAts q  -> MAts (find_ts th q)
          | PMAls q  -> MAls (find_ls th q)
          | PMApr q  -> MApr (find_pr th q)
          | PMAstr s -> MAstr s
          | PMAint i -> MAint i
        in
143 144
        let m = lookup_meta s in
        let td = create_meta m (List.map convert al) in
145
        add_meta th td (if c then meta_cl else meta)
146
  in
147 148
  let add_local th (loc,rule) =
    try add_local th rule with e -> raise (Loc.Located (loc,e))
149 150 151
  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
152 153
    let th =
      try Env.find_theory env f id with e -> raise (Loc.Located (loc,e))
154 155 156 157 158
    in
    qualid := q;
    List.iter (add_local th) trl
  in
  List.iter add_theory f.f_rules;
159 160
  transform := List.rev !transform;
  incr driver_tag;
161
  {
162 163 164 165 166 167
    drv_env       = env;
    drv_printer   = !printer;
    drv_prelude   = !prelude;
    drv_filename  = !filename;
    drv_transform = !transform;
    drv_thprelude = !thprelude;
168 169
    drv_meta      = !meta;
    drv_meta_cl   = !meta_cl;
170 171
    drv_regexps   = !regexps;
    drv_exitcodes = !exitcodes;
172
  }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
173

174
(** apply drivers *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
175

176
exception UnknownSpec of string
177

178 179 180 181 182 183 184
let filename_regexp = Str.regexp "%\\(.\\)"

let get_filename drv input_file theory_name goal_name =
  let file = match drv.drv_filename with
    | Some f -> f
    | None -> "%f-%t-%g.dump"
  in
185
  let replace s = match Str.matched_group 1 s with
186 187 188
    | "%" -> "%"
    | "f" -> input_file
    | "t" -> theory_name
189
    | "g" -> goal_name
190
    | s   -> raise (UnknownSpec s)
191
  in
192
  Str.global_substitute filename_regexp replace file
193

194
let file_of_task drv input_file theory_name task =
195
  get_filename drv input_file theory_name (task_goal task).pr_name.id_string
196

197
let call_on_buffer ~command ?timelimit ?memlimit drv buffer =
198 199 200 201
  let regexps = drv.drv_regexps in
  let exitcodes = drv.drv_exitcodes in
  let filename = get_filename drv "" "" "" in
  Call_provers.call_on_buffer
202
    ~command ?timelimit ?memlimit ~regexps ~exitcodes ~filename buffer
203

204 205 206 207
(** print'n'prove *)

exception NoPrinter

208 209 210 211
let update_task drv task =
  let task, goal = match task with
    | Some { task_decl = g ; task_prev = t } -> t,g
    | None -> raise Task.GoalNotFound
212 213 214 215 216
  in
  let task =
    Mid.fold (fun _ (th,s) task ->
      let cs = (find_clone task th).tds_set in
      Stdecl.fold (fun td task -> match td.td_node with
217 218
        | Clone (_,tm,lm,pm)
          when Mts.is_empty tm && Mls.is_empty lm && Mpr.is_empty pm ->
219
            Stdecl.fold (fun td task -> add_tdecl task td) s task
220
        | _ -> task
221 222 223 224 225 226 227 228 229 230 231 232 233
      ) cs task
    ) drv.drv_meta task
  in
  let task =
    Mid.fold (fun _ (th,s) task ->
      let cs = (find_clone task th).tds_set in
      Stdecl.fold (fun tdc task ->
        Stdecl.fold (fun tdm task ->
          add_tdecl task (clone_meta tdm th tdc)
        ) s task
      ) cs task
    ) drv.drv_meta_cl task
  in
234 235
  add_tdecl task goal

236
let print_task drv fmt task =
237 238 239 240
  let p = match drv.drv_printer with
    | None -> raise NoPrinter
    | Some p -> p
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
241
  let printer = lookup_printer p drv.drv_prelude drv.drv_thprelude in
242 243
  let lookup_transform t = t, lookup_transform t drv.drv_env in
  let transl = List.map lookup_transform drv.drv_transform in
244
  let apply task (t, tr) =
245
(*  Format.printf "@\n@\n[%f] %s@." (Sys.time ()) t; *)
246
    Trans.apply_named t tr task
247
  in
248 249 250 251
(*Format.printf "@\n@\nTASK";*)
  let task = update_task drv task in
  let task = List.fold_left apply task transl in
  fprintf fmt "@[%a@]@?" printer task
252

253
let prove_task ~command ?timelimit ?memlimit drv task =
254 255
  let buf = Buffer.create 1024 in
  let fmt = formatter_of_buffer buf in
256 257
  print_task drv fmt task; pp_print_flush fmt ();
  call_on_buffer ~command ?timelimit ?memlimit drv buf
258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280

(* 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"
  | NoPlugins -> Format.fprintf fmt
      "Plugins are not supported, recomplie Why"
  | 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
  | e -> raise e)