driver.ml 11.1 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
MARCHE Claude's avatar
MARCHE Claude committed
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
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 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;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
47
}
48

49 50
(** parse a driver file *)

51 52
exception NoPlugins

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
59
let load_file file =
60
  let basename = Filename.dirname file in
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
61 62 63
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
64 65 66 67 68 69 70 71 72 73 74 75
  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;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76
  f
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
77

78 79 80 81
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)
82 83
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
84

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

94
  let set_or_raise loc r v error = match !r with
95
    | Some _ -> raise (Loc.Located (loc, Duplicate error))
96 97 98
    | None   -> r := Some v
  in
  let add_to_list r v = (r := v :: !r) in
99
  let add_global (loc, g) = match g with
100 101 102 103 104 105
    | 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)
106
    | TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
107 108 109 110 111
    | 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)
112
    | Filename s -> set_or_raise loc filename s "filename"
113 114
    | Printer s -> set_or_raise loc printer s "printer"
    | Transform s -> add_to_list transform s
115
    | Plugin files -> load_plugin (Filename.dirname file) files
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116
  in
117
  let f = load_file file in
118 119 120
  List.iter add_global f.f_global;

  let thprelude = ref Mid.empty in
121 122
  let meta      = ref Mid.empty in
  let meta_cl   = ref Mid.empty in
123 124
  let qualid    = ref [] in

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

200
(** apply drivers *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
201

202
exception UnknownSpec of string
203

204 205 206 207 208 209 210
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
211
  let replace s = match Str.matched_group 1 s with
212 213 214
    | "%" -> "%"
    | "f" -> input_file
    | "t" -> theory_name
215
    | "g" -> goal_name
216
    | s   -> raise (UnknownSpec s)
217
  in
218
  Str.global_substitute filename_regexp replace file
219

220
let file_of_task drv input_file theory_name task =
221
  get_filename drv input_file theory_name (task_goal task).pr_name.id_string
222

223
let call_on_buffer ~command ?timelimit ?memlimit drv buffer =
224
  let regexps = drv.drv_regexps in
225
  let timeregexps = drv.drv_timeregexps in
226 227 228
  let exitcodes = drv.drv_exitcodes in
  let filename = get_filename drv "" "" "" in
  Call_provers.call_on_buffer
229
    ~command ?timelimit ?memlimit ~regexps ~timeregexps
230
    ~exitcodes ~filename buffer
231

232 233 234 235
(** print'n'prove *)

exception NoPrinter

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

261
let prepare_task drv task =
Andrei Paskevich's avatar
Andrei Paskevich committed
262
  let lookup_transform t = lookup_transform t drv.drv_env in
263
  let transl = List.map lookup_transform drv.drv_transform in
Andrei Paskevich's avatar
Andrei Paskevich committed
264
  let apply task tr = Trans.apply tr task in
265
  let task = update_task drv task in
Andrei Paskevich's avatar
Andrei Paskevich committed
266
  List.fold_left apply task transl
267 268 269 270 271 272 273 274 275 276


let print_task_prepared ?old drv fmt task =
  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
277
  fprintf fmt "@[%a@]@?" (printer ?old) task
278

279 280 281 282 283 284

let print_task ?old drv fmt task =
  let task = prepare_task drv task in
  print_task_prepared ?old drv fmt task

let prove_task_prepared ~command ?timelimit ?memlimit ?old drv task =
285 286
  let buf = Buffer.create 1024 in
  let fmt = formatter_of_buffer buf in
287
  print_task_prepared ?old drv fmt task; pp_print_flush fmt ();
288 289 290
  let res = call_on_buffer ~command ?timelimit ?memlimit drv buf in
  Buffer.reset buf;
  res
291

292 293 294 295 296

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

297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316
(* 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
317 318 319 320
  | 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
321 322
  | e -> raise e)