driver.ml 9.78 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 46
  drv_prelude   : prelude;
  drv_thprelude : prelude_map;
  drv_syntax    : syntax_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
47
}
48

49 50
(** parse a driver file *)

51 52
exception NoPlugins

53
let load_plugin dir (byte,nat) =
54
  if not Config.why_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 =
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
60 61 62
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
63
  let f = Driver_lexer.parse_file lb in
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
64
  close_in c;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
65
  f
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
66

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

72
let load_driver = let driver_tag = ref (-1) in fun env file ->
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

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

  let thprelude = ref Mid.empty in
  let syntax    = ref Mid.empty in
107 108
  let meta      = ref Mid.empty in
  let meta_cl   = ref Mid.empty in
109 110
  let qualid    = ref [] in

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

177
(** apply drivers *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
178

179
exception UnknownSpec of string
180

181 182 183 184 185 186 187
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
188
  let replace s = match Str.matched_group 1 s with
189 190 191
    | "%" -> "%"
    | "f" -> input_file
    | "t" -> theory_name
192
    | "g" -> goal_name
193
    | s   -> raise (UnknownSpec s)
194
  in
195
  Str.global_substitute filename_regexp replace file
196

197
let file_of_task drv input_file theory_name task =
198
  get_filename drv input_file theory_name (task_goal task).pr_name.id_string
199

200
let call_on_buffer ?debug ~command ?timelimit ?memlimit drv buffer =
201 202 203 204
  let regexps = drv.drv_regexps in
  let exitcodes = drv.drv_exitcodes in
  let filename = get_filename drv "" "" "" in
  Call_provers.call_on_buffer
205
    ?debug ~command ?timelimit ?memlimit ~regexps ~exitcodes ~filename buffer
206

207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277
(** print'n'prove *)

exception NoPrinter
exception TransFailure of (string * exn)

let print_task ?(debug=false) drv fmt task =
  let p = match drv.drv_printer with
    | None -> raise NoPrinter
    | Some p -> p
  in
  let printer =
    lookup_printer p drv.drv_prelude drv.drv_thprelude drv.drv_syntax
  in
  let lookup_transform t = t, lookup_transform t drv.drv_env in
  let transl = List.map lookup_transform drv.drv_transform 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
        | Clone (_,cl) when Mid.is_empty cl ->
            Stdecl.fold (fun td task -> add_tdecl task td) s task
        | _ -> assert false (* impossible *)
      ) 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
  let apply task (t, tr) =
    try Trans.apply tr task
    with e when not debug -> raise (TransFailure (t,e))
  in
  fprintf fmt "@[%a@]@?" printer (List.fold_left apply task transl)

let prove_task ?debug ~command ?timelimit ?memlimit drv task =
  let buf = Buffer.create 1024 in
  let fmt = formatter_of_buffer buf in
  print_task ?debug drv fmt task; pp_print_flush fmt ();
  call_on_buffer ?debug ~command ?timelimit ?memlimit drv buf

(* 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
  | TransFailure (s,e) -> Format.fprintf fmt
      "Failure in transformation %s@\n%a" s Exn_printer.exn_printer e
  | 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)