why3extract.ml 10.8 KB
Newer Older
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  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10 11 12 13 14
(********************************************************************)

open Format
open Why3
open Stdlib
15
open Pmodule
16
open Compile
17 18

let usage_msg = sprintf
Mário Pereira's avatar
Mário Pereira committed
19 20
  "Usage: %s [options] -D <driver> [-o <dir|file>] \
             [<file>.<Module>*.<symbol>?|-]"
21 22
  (Filename.basename Sys.argv.(0))

Mário Pereira's avatar
Mário Pereira committed
23 24
type extract_target =
  | File   of string
25 26
  | Module of string list * string
  | Symbol of string list * string * string
Mário Pereira's avatar
Mário Pereira committed
27

28 29
let opt_queue = Queue.create ()

Mário Pereira's avatar
Mário Pereira committed
30
(* let opt_input = ref None *)
31

Mário Pereira's avatar
Mário Pereira committed
32 33 34 35 36 37 38 39 40 41
let opt_parser = ref None
let opt_output = ref None
let opt_driver = ref []

type recurs_single = Recursive | Single
let opt_rec_single = ref Single

type flat_modular = Flat | Modular
let opt_modu_flat = ref Flat

Mário Pereira's avatar
Mário Pereira committed
42
let is_uppercase c = c = Char.uppercase_ascii c
43

44
let add_opt_file x =
45 46 47 48 49 50 51 52 53 54 55 56 57
  let invalid_path () = Format.eprintf "invalid path: %s@." x; exit 1 in
  let target =
    if Sys.file_exists x then File x else
      let path = Strings.split '.' x in
      if path = [] then invalid_path ();
      let path, s = Lists.chop_last path in
      if String.length s = 0 then invalid_path ();
      if is_uppercase s.[0] then Module (path, s) else
      begin
        if path = [] then invalid_path ();
        let path, m = Lists.chop_last path in
        Symbol (path, m, s)
      end in
Mário Pereira's avatar
Mário Pereira committed
58
  Queue.push (Some target) opt_queue
59 60 61

let option_list = [
  "-", Arg.Unit (fun () -> add_opt_file "-"),
Andrei Paskevich's avatar
Andrei Paskevich committed
62
      " read the input file from stdin";
63
  "-F", Arg.String (fun s -> opt_parser := Some s),
Andrei Paskevich's avatar
Andrei Paskevich committed
64
      "<format> select input format (default: \"why\")";
65 66
  "--format", Arg.String (fun s -> opt_parser := Some s),
      " same as -F";
67 68 69
  "-D", Arg.String (fun s -> opt_driver := s::!opt_driver),
      "<file> specify an extraction driver";
  "--driver", Arg.String (fun s -> opt_driver := s::!opt_driver),
70
      " same as -D";
Mário Pereira's avatar
Mário Pereira committed
71
  "--recursive", Arg.Unit (fun () -> opt_rec_single := Recursive),
Mário Pereira's avatar
Mário Pereira committed
72 73 74
      " recursively extract all dependencies";
  "--flat", Arg.Unit (fun x -> x),
      " perform a flat extraction (default option)";
Mário Pereira's avatar
Mário Pereira committed
75 76
  "--modular", Arg.Unit (fun () -> opt_modu_flat := Modular),
      " perform a modular extraction";
77
  "-o", Arg.String (fun s -> opt_output := Some s),
78
      "<file|dir> destination of extracted code";
79 80 81
  "--output", Arg.String (fun s -> opt_output := Some s),
      " same as -o" ]

82
let config, _, env =
Andrei Paskevich's avatar
Andrei Paskevich committed
83
  Whyconf.Args.initialize option_list add_opt_file usage_msg
84 85

let () =
Mário Pereira's avatar
Mário Pereira committed
86
  if Queue.is_empty opt_queue then begin
Andrei Paskevich's avatar
Andrei Paskevich committed
87
    Whyconf.Args.exit_with_usage option_list usage_msg
Mário Pereira's avatar
Mário Pereira committed
88
  end
89

Mário Pereira's avatar
Mário Pereira committed
90 91 92
let opt_rec_single = !opt_rec_single
let opt_modu_flat  = !opt_modu_flat

Mário Pereira's avatar
Mário Pereira committed
93 94 95 96 97 98 99 100 101 102
let opt_output = match opt_modu_flat, !opt_output with
  | Modular, None ->
    eprintf "Output directory (-o) is required for modular extraction.@.";
    exit 1
  | Modular, Some s when not (Sys.file_exists s) ->
    eprintf "Option '-o' should be given an existing directory as argument.@.";
    exit 1
  | Modular, Some s when not (Sys.is_directory s) ->
    eprintf "Option '-o' should be given a directory as argument.@.";
    exit 1
Mário Pereira's avatar
Mário Pereira committed
103 104
  | Flat, Some s when Sys.file_exists s && Sys.is_directory s ->
    eprintf "Option '-o' should be given a file as argument.@.";
Mário Pereira's avatar
Mário Pereira committed
105 106 107
    exit 1
  | Modular, Some _ | Flat, None | Flat, Some _ -> !opt_output

108 109 110 111
let driver_file s =
  if Sys.file_exists s || String.contains s '/' || String.contains s '.' then s
  else Filename.concat Config.datadir (Filename.concat "drivers" (s ^ ".drv"))

112
let opt_driver =
113 114 115
  try match List.rev_map driver_file !opt_driver with
  | [] ->
    eprintf "Extraction driver (-D) is required.@.";
116
    exit 1
117
  | f::ef ->
118
    Pdriver.load_driver env f ef
119 120 121
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
122

Mário Pereira's avatar
Mário Pereira committed
123 124 125
let get_cout_old ?fname fg m = match opt_output with
  | None ->
    let tname = m.mod_theory.Theory.th_name.Ident.id_string in
Mário Pereira's avatar
Mário Pereira committed
126
    Debug.dprintf Pdriver.debug "extract module %s to standard output@." tname;
Mário Pereira's avatar
Mário Pereira committed
127 128 129 130 131 132
    stdout, None
  | Some f ->
    let file = Filename.concat f (fg ?fname m) in
    let tname = m.mod_theory.Theory.th_name.Ident.id_string in
    Debug.dprintf Pdriver.debug "extract module %s to file %s@." tname file;
    let old = if Sys.file_exists file then begin
133 134 135
      let backup = file ^ ".bak" in
      Sys.rename file backup;
      Some (open_in backup) end else None in
Mário Pereira's avatar
Mário Pereira committed
136 137
    open_out file, old

Mário Pereira's avatar
Mário Pereira committed
138
let print_mdecls ?fname m mdecls =
139
  let (fg,pargs,pr) = Pdriver.lookup_printer opt_driver in
Mário Pereira's avatar
Mário Pereira committed
140 141 142 143 144 145 146 147 148 149 150
  let test_decl_not_driver decl =
    let decl_name = ML.get_decl_name decl in
    let test_id_not_driver id =
      Printer.query_syntax pargs.Pdriver.syntax id = None in
    List.exists test_id_not_driver decl_name in
  if List.exists test_decl_not_driver mdecls then begin
    let cout, old = get_cout_old fg m ?fname in
    let fmt = formatter_of_out_channel cout in
    let flat = opt_modu_flat = Flat in
    List.iter (pr pargs ?old ?fname ~flat m fmt) mdecls;
    if cout <> stdout then close_out cout end
Mário Pereira's avatar
Mário Pereira committed
151

Mário Pereira's avatar
Mário Pereira committed
152 153 154 155 156 157 158 159 160 161 162
let find_module_path mm path m = match path with
  | [] ->
    Mstr.find m mm
  | path ->
    let mm = Env.read_library Pmodule.mlw_language env path in
    Mstr.find m mm

let find_module_id mm id =
  let (path, m, _) = Pmodule.restore_path id in
  find_module_path mm path m

Mário Pereira's avatar
Mário Pereira committed
163 164 165
let translate_module =
  let memo = Ident.Hid.create 16 in
  fun m ->
166
    let name = m.mod_theory.Theory.th_name in
Mário Pereira's avatar
Mário Pereira committed
167 168 169 170 171 172
    try Ident.Hid.find memo name with Not_found ->
      let pm, info = Translate.module_ m in
      let pm       = Transform.module_ info pm in
      Ident.Hid.add memo name pm;
      pm

173 174 175 176 177 178 179 180
let extract_to =
  let memo = Ident.Hid.create 16 in
  fun ?fname ?decl m ->
    let name = m.mod_theory.Theory.th_name in
    if not (Ident.Hid.mem memo name) then begin
      Ident.Hid.add memo name ();
      let mdecls = match decl with
        | None   -> (translate_module m).ML.mod_decl
Mário Pereira's avatar
Mário Pereira committed
181
        | Some d -> Translate.pdecl_m m d in
182 183
      print_mdecls ?fname m mdecls
    end
184

185
let rec use_iter f l =
186 187
  List.iter
    (function Uuse t -> f t | Uscope (_,_,l) -> use_iter f l | _ -> ()) l
188

189
let rec do_extract_module ?fname m =
Mário Pereira's avatar
Mário Pereira committed
190
  let extract_use m' =
191 192 193 194 195
    let fname =
      if m'.mod_theory.Theory.th_path = [] then fname else None
    in
    do_extract_module ?fname m'
  in
Mário Pereira's avatar
Mário Pereira committed
196
  begin match opt_rec_single with
Mário Pereira's avatar
Mário Pereira committed
197 198
  | Recursive -> use_iter extract_use m.mod_units
  | Single -> ()
199
  end;
200
  extract_to ?fname m
201

Mário Pereira's avatar
Mário Pereira committed
202 203 204 205
(* let do_global_extract (_,p,t) = *)
(*   let env = opt_driver.Pdriver.drv_env in *)
(*   let m = read_module env p t in *)
(*   do_extract_module m *)
206

Mário Pereira's avatar
Mário Pereira committed
207
let do_extract_module_from fname mm m =
208
  try
Mário Pereira's avatar
Mário Pereira committed
209
    let m = Mstr.find m mm in do_extract_module ~fname m
210
  with Not_found ->
Mário Pereira's avatar
Mário Pereira committed
211
    eprintf "Module '%s' not found in file '%s'.@." m fname;
212 213
    exit 1

Mário Pereira's avatar
Mário Pereira committed
214 215 216 217
let get_symbol ns find str_symbol =
  try let symbol = find ns [str_symbol] in Some symbol
  with Not_found -> None

218
let find_symbol_id ns str_symbol =
Mário Pereira's avatar
Mário Pereira committed
219
  match get_symbol ns ns_find_rs str_symbol with
Mário Pereira's avatar
Mário Pereira committed
220 221 222 223 224 225 226
    | Some rs -> rs.Expr.rs_name
    | None -> (* creative indentation *)
    begin match get_symbol ns ns_find_its str_symbol with
    | Some its -> its.Ity.its_ts.Ty.ts_name
    | None -> (* creative indentation *)
    begin match get_symbol ns ns_find_xs str_symbol with
    | Some xs -> xs.Ity.xs_name
227
    | None -> raise Not_found
Mário Pereira's avatar
Mário Pereira committed
228 229 230 231 232 233 234
    end end

let find_pmod m mlw_file fname =
  try Mstr.find m mlw_file with Not_found ->
    eprintf "Module '%s' not found in the file '%s'.@." m fname;
    exit 1

235 236 237 238 239
let do_extract_symbol_from ?fname m str_symbol =
  let ns = m.mod_export in
  let id = find_symbol_id ns str_symbol in
  let decl = Ident.Mid.find id m.mod_known in
  extract_to ?fname ~decl m
Mário Pereira's avatar
Mário Pereira committed
240 241 242 243 244 245

let read_mlw_file ?format env fname =
  let cin = open_in fname in
  let mm = Env.read_channel ?format mlw_language env fname cin in
  close_in cin;
  mm
Mário Pereira's avatar
Mário Pereira committed
246 247

let do_local_extract target =
Andrei Paskevich's avatar
Andrei Paskevich committed
248
  let format = !opt_parser in
Mário Pereira's avatar
Mário Pereira committed
249
  match target with
Mário Pereira's avatar
Mário Pereira committed
250 251
  | File fname ->
    let mm = read_mlw_file ?format env fname in
MARCHE Claude's avatar
MARCHE Claude committed
252
    let do_m _ m = do_extract_module ~fname m in
Mário Pereira's avatar
Mário Pereira committed
253
    Mstr.iter do_m mm
254 255 256 257 258 259 260 261
  | Module (path, m) ->
    let mm = Mstr.empty in
    let m = find_module_path mm path m in
    do_extract_module m
  | Symbol (path, m, s) ->
    let mm = Mstr.empty in
    let m = find_module_path mm path m in
    do_extract_symbol_from m s
262 263

let do_input = function
Mário Pereira's avatar
Mário Pereira committed
264 265
  | None -> assert false (*TODO*)
    (* Queue.iter do_global_extract tlist *)
Mário Pereira's avatar
Mário Pereira committed
266 267
  | Some target ->
    do_local_extract target
268

Mário Pereira's avatar
Mário Pereira committed
269
let visited = Ident.Hid.create 1024
270 271
let toextract = ref []

272 273 274 275
let find_decl mm id =
  let m = find_module_id mm id in
  let m = translate_module m in
  Ident.Mid.find id m.ML.mod_known
Mário Pereira's avatar
Mário Pereira committed
276

Mário Pereira's avatar
Mário Pereira committed
277
let rec visit mm id =
Mário Pereira's avatar
Mário Pereira committed
278
  if not (Ident.Hid.mem visited id) then begin
Mário Pereira's avatar
Mário Pereira committed
279 280 281 282 283 284 285
    try
      let d = find_decl mm id in
      (* Can I change these the two lines (* *) ? *)
      Ident.Hid.add visited id (); (* *)
      ML.iter_deps (visit mm) d;   (* *)
      toextract := id :: !toextract
    with Not_found -> ()
286
  end
287

288 289 290 291
let visit mm id =
  if opt_rec_single = Recursive then visit mm id
  else toextract := id :: !toextract

Mário Pereira's avatar
Mário Pereira committed
292
let flat_extraction target = match Opt.get target with
Mário Pereira's avatar
Mário Pereira committed
293 294 295 296 297
  | File fname ->
    let format = !opt_parser in
    let mm = read_mlw_file ?format env fname in
    let do_m _ m = do_extract_module ~fname m in
    Mstr.iter do_m mm
298 299 300 301 302 303 304 305 306 307 308
  | Module (path, m) ->
    let mm = Mstr.empty in
    let m = find_module_path mm path m in
    let m = translate_module m in
    Ident.Mid.iter (fun id _ -> visit mm id) m.ML.mod_known
  | Symbol (path, m, s) ->
    let mm = Mstr.empty in
    let m = find_module_path mm path m in
    let ns = m.mod_export in
    let id = find_symbol_id ns s in
    visit mm id
309

310 311
let () =
  try
Mário Pereira's avatar
Mário Pereira committed
312
    match opt_modu_flat with
Mário Pereira's avatar
Mário Pereira committed
313
    | Modular -> Queue.iter do_input opt_queue
314 315 316 317
    | Flat ->
      Queue.iter flat_extraction opt_queue;
      let (_fg, pargs, pr) = Pdriver.lookup_printer opt_driver in
      let mm = Mstr.empty in
Mário Pereira's avatar
Mário Pereira committed
318
      let cout = match opt_output with
Mário Pereira's avatar
Mário Pereira committed
319 320
        | None -> stdout
        | Some file -> open_out file in
Mário Pereira's avatar
Mário Pereira committed
321
      let fmt = formatter_of_out_channel cout in
Mário Pereira's avatar
Mário Pereira committed
322
      let extract fmt id =
323 324 325
        let pm = find_module_id mm id in
        let m = translate_module pm in
        let d = Ident.Mid.find id m.ML.mod_known in
Mário Pereira's avatar
Mário Pereira committed
326
        pr pargs ~flat:true pm fmt d in
Mário Pereira's avatar
Mário Pereira committed
327
      List.iter (extract fmt) (List.rev !toextract);
Mário Pereira's avatar
Mário Pereira committed
328
      if cout <> stdout then close_out cout
329 330 331
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
332 333 334 335 336 337

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3extract.opt"
End:
*)