driver.ml 12.3 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.                  *)
(*                                                                        *)
(**************************************************************************)

Andrei Paskevich's avatar
Andrei Paskevich committed
20 21
open Util
open Ident
22 23
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
24
open Decl
25
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
26
open Task
Francois Bobot's avatar
Francois Bobot committed
27
open Register
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
28
open Driver_ast
29
open Call_provers
30

31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
(** error handling *)

type error = string

exception Error of string

let report = Format.pp_print_string

let error ?loc e = match loc with
  | None -> raise (Error e)
  | Some loc -> raise (Loc.Located (loc, Error e))

let errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
  Format.kfprintf
    (fun _ ->
       Format.pp_print_flush fmt ();
       let s = Buffer.contents buf in
       Buffer.clear buf;
       error ?loc s)
    fmt f

(** syntax substitutions *)
55 56

let opt_search_forward re s pos =
57
  try Some (Str.search_forward re s pos) with Not_found -> None
58

59
let global_substitute_fmt expr repl_fun text fmt =
60 61 62
  let rec replace start last_was_empty =
    let startpos = if last_was_empty then start + 1 else start in
    if startpos > String.length text then
63
      Format.pp_print_string fmt (Str.string_after text start)
64 65 66
    else
      match opt_search_forward expr text startpos with
      | None ->
67
          Format.pp_print_string fmt (Str.string_after text start)
68
      | Some pos ->
69 70
          let end_pos = Str.match_end () in
          Format.pp_print_string fmt (String.sub text start (pos - start));
71 72 73
          repl_fun text fmt;
          replace end_pos (end_pos = pos)
  in
74
  replace 0 false
75 76 77 78 79 80

let iter_group expr iter_fun text =
  let rec iter start last_was_empty =
    let startpos = if last_was_empty then start + 1 else start in
    if startpos < String.length text then
      match opt_search_forward expr text startpos with
81 82 83 84 85
      | None -> ()
      | Some pos ->
          let end_pos = Str.match_end () in
          iter_fun text;
          iter end_pos (end_pos = pos)
86 87
  in
  iter 0 false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
88

89
let regexp_arg_pos = Str.regexp "%\\([0-9]+\\)"
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90

91 92 93 94 95 96 97 98
let check_syntax loc s len =
  let arg s =
    let i = int_of_string (Str.matched_group 1 s) in
    if i = 0 then errorm ~loc "bad index '%%0': start with '%%1'";
    if i > len then
      errorm ~loc "bad index '%%%i': the symbol has %i arguments" i len
  in
  iter_group regexp_arg_pos arg s
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
99

100 101 102 103 104 105
let syntax_arguments s print fmt l =
  let args = Array.of_list l in
  let repl_fun s fmt =
    let i = int_of_string (Str.matched_group 1 s) in
    print fmt args.(i-1) in
  global_substitute_fmt regexp_arg_pos repl_fun s fmt
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
106

107
(** drivers *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108

109
type translation =
110 111
  | Remove
  | Syntax of string
Andrei Paskevich's avatar
Andrei Paskevich committed
112
  | Tag of Sstr.t
113

114 115 116 117
let translation_union t1 t2 = match t1, t2 with
  | Remove, _ | _, Remove -> Remove
  | ((Syntax _ as s), _) | (_,(Syntax _ as s)) -> s
  | Tag s1, Tag s2 -> Tag (Sstr.union s1 s2)
118 119

let print_translation fmt = function
120 121 122
  | Remove -> Format.fprintf fmt "remove"
  | Syntax s -> Format.fprintf fmt "syntax %s" s
  | Tag s -> Format.fprintf fmt "tag %a"
Andrei Paskevich's avatar
Andrei Paskevich committed
123
      (Pp.print_iter1 Sstr.iter Pp.comma Pp.string) s
124

125
type printer = (ident -> translation) -> Format.formatter -> task -> unit
126

127
type driver = {
128
  drv_env          : Env.env;
129 130 131
  drv_printer      : printer option;
  drv_prelude      : string list;
  drv_filename     : string option;
132
  drv_transform    : task trans_reg;
133
  drv_thprelude    : string list Mid.t;
134
  drv_translations : (translation * translation) Mid.t;
135
  drv_regexps      : (Str.regexp * Call_provers.prover_answer) list;
136
  drv_exitcodes    : (int * Call_provers.prover_answer) list;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
137
}
138

139
(** register printers and transformations *)
140

141
let printers : (string, printer) Hashtbl.t = Hashtbl.create 17
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
142
let register_printer name printer = Hashtbl.replace printers name printer
Francois Bobot's avatar
 
Francois Bobot committed
143 144
let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers []

145 146 147 148 149 150 151 152
let transforms : (string, task trans_reg) Hashtbl.t = Hashtbl.create 17
let register_transform name trans = Hashtbl.replace transforms name trans
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []

let transforms_l : (string, task tlist_reg) Hashtbl.t = Hashtbl.create 17
let register_transform_l name trans = Hashtbl.replace transforms_l name trans
let list_transforms_l () = Hashtbl.fold (fun k _ ac -> k::ac) transforms_l []

153 154
(** parse a driver file *)

155
let load_plugin dir (byte,nat) =
Andrei Paskevich's avatar
Andrei Paskevich committed
156
  if not Config.why_plugins then errorm "Plugins not supported";
Andrei Paskevich's avatar
Andrei Paskevich committed
157
  let file = if Config.Dynlink.is_native then nat else byte in
158
  let file = Filename.concat dir file in
Andrei Paskevich's avatar
Andrei Paskevich committed
159
  Config.Dynlink.loadfile_private file
160

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
161
let load_file file =
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
162 163 164
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
165
  let f = Driver_lexer.parse_file lb in
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
166
  close_in c;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
167
  f
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
168

169
let string_of_qualid thl idl =
170
  String.concat "." thl ^ "." ^ String.concat "." idl
171

172 173 174 175 176
let add_htheory tmap cloned id t =
  try
    let t2,t3 = Mid.find id tmap in
    let t23 = if cloned
      then translation_union t t2, t3
177
      else t2, translation_union t t3
178
    in
179
    Mid.add id t23 tmap
180
  with Not_found ->
181 182 183
    let t23 = if cloned
      then Tag Sstr.empty, t
      else t, Tag Sstr.empty
184
    in
185
    Mid.add id t23 tmap
186

187
let load_rules env (pmap,tmap) { thr_name = (loc,qualid); thr_rules = trl } =
188 189
  let qfile,id = let l = List.rev qualid in List.rev (List.tl l),List.hd l in
  let th = try Env.find_theory env qfile id with Env.TheoryNotFound (l,s) ->
190 191
    errorm ~loc "theory %s.%s not found" (String.concat "." l) s
  in
192 193 194 195 196 197 198 199 200
  let find_pr (loc,q) = try ns_find_pr th.th_export q with Not_found ->
    errorm ~loc "Unknown proposition %s" (string_of_qualid qualid q)
  in
  let find_ls (loc,q) = try ns_find_ls th.th_export q with Not_found ->
    errorm ~loc "Unknown logic symbol %s" (string_of_qualid qualid q)
  in
  let find_ts (loc,q) = try ns_find_ts th.th_export q with Not_found ->
    errorm ~loc "Unknown type symbol %s" (string_of_qualid qualid q)
  in
201 202
  let add (pmap,tmap) (loc,rule) = match rule with
    | Rremove (c,q) ->
203 204 205 206 207 208 209 210 211 212 213 214 215
        pmap, add_htheory tmap c (find_pr q).pr_name Remove
    | Rsyntaxls (q,s) -> let ls = find_ls q in
        check_syntax loc s (List.length ls.ls_args);
        pmap, add_htheory tmap false ls.ls_name (Syntax s)
    | Rsyntaxty (q,s) -> let ts = find_ts q in
        check_syntax loc s (List.length ts.ts_args);
        pmap, add_htheory tmap false ts.ts_name (Syntax s)
    | Rtagls (c,q,s) ->
        pmap, add_htheory tmap c (find_ls q).ls_name (Tag (Sstr.singleton s))
    | Rtagty (c,q,s) ->
        pmap, add_htheory tmap c (find_ts q).ts_name (Tag (Sstr.singleton s))
    | Rtagpr (c,q,s) ->
        pmap, add_htheory tmap c (find_pr q).pr_name (Tag (Sstr.singleton s))
216
    | Rprelude s ->
217 218
        let l = try Mid.find th.th_name pmap with Not_found -> [] in
        Mid.add th.th_name (s::l) pmap, tmap
MARCHE Claude's avatar
MARCHE Claude committed
219
  in
220
  List.fold_left add (pmap,tmap) trl
221

222
let load_driver env file =
223 224 225 226 227
  let prelude   = ref [] in
  let regexps   = ref [] in
  let exitcodes = ref [] in
  let filename  = ref None in
  let printer   = ref None in
228
  let transform = ref identity in
229 230 231 232 233
  let set_or_raise loc r v error = match !r with
    | Some _ -> errorm ~loc "duplicate %s" error
    | None   -> r := Some v
  in
  let add_to_list r v = (r := v :: !r) in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
234
  let add (loc, g) = match g with
235 236 237 238 239 240 241 242 243 244 245
    | 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)
246
    | Filename s -> set_or_raise loc filename s "filename"
247
    | Printer s -> begin
248 249 250
        try set_or_raise loc printer (Hashtbl.find printers s) "printer"
        with Not_found -> errorm ~loc "unknown printer %s" s end
    | Transform s -> begin
251
        try transform := compose (Hashtbl.find transforms s) !transform
252
        with Not_found -> errorm ~loc "unknown transformation %s" s end
253
    | Plugin files -> load_plugin (Filename.dirname file) files
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
254
  in
255
  let f = load_file file in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
256
  List.iter add f.f_global;
257 258
  let (pmap,tmap) =
      List.fold_left (load_rules env) (Mid.empty,Mid.empty) f.f_rules
259
  in
260
  {
261 262 263 264
    drv_env          = env;
    drv_printer      = !printer;
    drv_prelude      = !prelude;
    drv_filename     = !filename;
265
    drv_transform    = !transform;
266
    drv_thprelude    = pmap;
267
    drv_translations = tmap;
268
    drv_regexps      = !regexps;
269
    drv_exitcodes    = !exitcodes;
270
  }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
271 272 273

(** querying drivers *)

274 275
let query_ident drv clone =
  let h = Hid.create 7 in
276
  fun id ->
277 278 279 280 281 282
    try
      Hid.find h id
    with Not_found ->
      let r = try
        Mid.find id clone
      with Not_found -> Sid.empty in
283 284 285 286 287
      let tr = try fst (Mid.find id drv.drv_translations)
      with Not_found -> Tag Sstr.empty in
      let tr = Sid.fold
        (fun id acc -> try translation_union acc
           (snd (Mid.find id drv.drv_translations))
288 289 290
         with Not_found -> acc) r tr in
      Hid.add h id tr;
      tr
291

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
292 293
(** using drivers *)

294
let print_prelude drv used fmt =
295
  let pr_pr s () = Format.fprintf fmt "%s@\n" s in
296
  List.fold_right pr_pr drv.drv_prelude ();
297 298
  let seen = Hid.create 17 in
  let rec print_prel th_name th =
Andrei Paskevich's avatar
Andrei Paskevich committed
299
    if Hid.mem seen th_name then () else begin
300 301
      Hid.add seen th_name ();
      Mid.iter print_prel th.th_used;
302 303
      let prel =
        try Mid.find th_name drv.drv_thprelude
304 305 306
        with Not_found -> []
      in
      List.fold_right pr_pr prel ()
Andrei Paskevich's avatar
Andrei Paskevich committed
307
    end
308
  in
309
  Mid.iter print_prel used;
310
  Format.fprintf fmt "@."
311

312
let print_task drv fmt task =
313
  let task = apply_env drv.drv_transform drv.drv_env task in
314 315 316 317 318 319
  let printer = match drv.drv_printer with
    | None -> errorm "no printer specified in the driver file"
    | Some p -> p (query_ident drv (task_clone task))
  in
  print_prelude drv (task_used task) fmt;
  Format.fprintf fmt "@[%a@]@?" printer task
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
320

321 322 323 324 325 326 327
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
328
  let replace s = match Str.matched_group 1 s with
329 330 331
    | "%" -> "%"
    | "f" -> input_file
    | "t" -> theory_name
332
    | "g" -> goal_name
333 334
    | _ -> errorm "unknown format specifier, use %%f, %%t or %%g"
  in
335
  Str.global_substitute filename_regexp replace file
336

337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352
let file_of_task drv input_file theory_name task =
  get_filename drv input_file theory_name (task_goal task).pr_name.id_short

let call_on_buffer ?debug ~command ~timelimit ~memlimit drv buffer =
  let regexps = drv.drv_regexps in
  let exitcodes = drv.drv_exitcodes in
  let filename = get_filename drv "" "" "" in
  Call_provers.call_on_buffer
    ?debug ~command ~timelimit ~memlimit ~regexps ~exitcodes ~filename buffer

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

353
(*
354
Local Variables:
355
compile-command: "unset LANG; make -C ../.. test"
356
End:
357
*)