Skip to content

GitLab

why3
why3
Commit abe18efd authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files
Options

Allow extraction of interface files

parent 80f84138
Hide whitespace changes
Inline Side-by-side
Showing with 246 additions and 128 deletions
drivers/c.drv
View file @ abe18efd
......@@ -77,7 +77,7 @@ struct __add32_with_carry_result
uint32_t __field_1;
};
struct __add32_with_carry_result add32_with_carry(uint32_t x, uint32_t y, uint32_t c)
static struct __add32_with_carry_result add32_with_carry(uint32_t x, uint32_t y, uint32_t c)
{
struct __add32_with_carry_result result;
uint64_t r = (uint64_t)x + (uint64_t)y + (uint64_t) c;
......@@ -91,7 +91,7 @@ struct __sub32_with_borrow_result
uint32_t __field_1;
};
struct __sub32_with_borrow_result sub32_with_borrow(uint32_t x, uint32_t y, uint32_t b)
static struct __sub32_with_borrow_result sub32_with_borrow(uint32_t x, uint32_t y, uint32_t b)
{
struct __sub32_with_borrow_result result;
uint64_t r = (uint64_t)x - (uint64_t)y - (uint64_t) b;
......@@ -105,7 +105,7 @@ struct __mul32_double_result
uint32_t __field_1;
};
struct __mul32_double_result mul32_double(uint32_t x, uint32_t y)
static struct __mul32_double_result mul32_double(uint32_t x, uint32_t y)
{
struct __mul32_double_result result;
uint64_t r = (uint64_t)x * (uint64_t)y;
......@@ -119,7 +119,7 @@ struct __add32_3_result
uint32_t __field_1;
};
struct __add32_3_result add32_3(uint32_t x, uint32_t y, uint32_t z)
static struct __add32_3_result add32_3(uint32_t x, uint32_t y, uint32_t z)
{
struct __add32_3_result result;
uint64_t r = (uint64_t)x + (uint64_t)y + (uint64_t) z;
......@@ -133,7 +133,7 @@ struct __lsld32_result
uint32_t __field_1;
};
struct __lsld32_result lsld32(uint32_t x, uint32_t cnt)
static struct __lsld32_result lsld32(uint32_t x, uint32_t cnt)
{
struct __lsld32_result result;
uint64_t r = (uint64_t)x << cnt;
......@@ -225,7 +225,7 @@ struct __add64_with_carry_result
uint64_t __field_1;
};
struct __add64_with_carry_result
static struct __add64_with_carry_result
add64_with_carry(uint64_t x, uint64_t y, uint64_t c)
{
struct __add64_with_carry_result result;
......@@ -241,7 +241,7 @@ struct __add64_double_result
uint64_t __field_1;
};
struct __add64_double_result
static struct __add64_double_result
add64_double(uint64_t a1, uint64_t a0, uint64_t b1, uint64_t b0)
{
struct __add64_double_result result;
......@@ -254,7 +254,7 @@ struct __sub64_with_borrow_result
uint64_t __field_1;
};
struct __sub64_with_borrow_result
static struct __sub64_with_borrow_result
sub64_with_borrow(uint64_t x, uint64_t y, uint64_t b)
{
struct __sub64_with_borrow_result result;
......@@ -271,7 +271,7 @@ struct __sub64_double_result
uint64_t __field_1;
};
struct __sub64_double_result
static struct __sub64_double_result
sub64_double(uint64_t a1, uint64_t a0, uint64_t b1, uint64_t b0)
{
struct __sub64_double_result result;
......@@ -284,14 +284,14 @@ struct __mul64_double_result
uint64_t __field_1;
};
struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)
static struct __mul64_double_result mul64_double(uint64_t x, uint64_t y)
{
struct __mul64_double_result result;
umul_ppmm(result.__field_1,result.__field_0,x,y);
return result;
}
uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
static uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d)
{
uint64_t q;
uint64_t _dummy __attribute__((unused));
......@@ -304,7 +304,7 @@ struct __add64_3_result
uint64_t __field_1;
};
struct __add64_3_result add64_3(uint64_t x, uint64_t y, uint64_t z)
static struct __add64_3_result add64_3(uint64_t x, uint64_t y, uint64_t z)
{
struct __add64_3_result result;
uint64_t r, c1, c2;
......@@ -322,7 +322,7 @@ struct __lsld64_result
uint64_t __field_1;
};
struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
static struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
{
struct __lsld64_result result;
result.__field_1 = x >> (64 - cnt);
......
src/mlw/cakeml_printer.ml
View file @ abe18efd
......@@ -474,13 +474,29 @@ let fg_cml ?fname m =
let path = m.mod_theory.th_path in
(module_name ?fname path mod_name) ^ ".cml"
let () = Pdriver.register_printer "cakeml"
~desc:"printer for CakeML code" fg_cml print_decl
open Pdriver
let cml_printer =
{ desc = "printer for CakeML code";
file_gen = fg_cml;
decl_printer = print_decl;
interf_gen = None;
interf_printer = None;
prelude_printer = print_empty_prelude }
let () = Pdriver.register_printer "cakeml" cml_printer
let fg_sml ?fname m =
let mod_name = m.mod_theory.th_name.id_string in
let path = m.mod_theory.th_path in
(module_name ?fname path mod_name) ^ ".sml"
let () = Pdriver.register_printer "sml"
~desc:"printer for SML code" fg_sml print_decl
let sml_printer =
{ desc = "printer for SML code";
file_gen = fg_sml;
decl_printer = print_decl;
interf_gen = None;
interf_printer = None;
prelude_printer = print_empty_prelude }
let () = Pdriver.register_printer "sml" sml_printer
src/mlw/cprinter.ml
View file @ abe18efd
......@@ -518,40 +518,45 @@ module Print = struct
and print_def fmt def =
try match def with
| Dfun (id,(rt,args),body) ->
fprintf fmt "%a %a(@[%a@])@ @[<hov>{@;<1 2>@[<hov>%a@]@\n}@\n@]"
let s = sprintf "%a %a(@[%a@])@ @[<hov>{@;<1 2>@[<hov>%a@]@\n}@\n@]"
(print_ty ~paren:false) rt
print_ident id
(print_list comma
(print_pair_delim nothing space nothing
(print_ty ~paren:false) print_ident))
args
print_body body
print_body body in
fprintf fmt "%s" s (* print into string first to print nothing in case of exception *)
| Dproto (id, (rt, args)) ->
fprintf fmt "%a %a(@[%a@]);@;"
(print_ty ~paren:false) rt
print_ident id
(print_list comma
(print_pair_delim nothing space nothing
(print_ty ~paren:false) print_ident))
args
let s = sprintf "%a %a(@[%a@]);@;"
(print_ty ~paren:false) rt
print_ident id
(print_list comma
(print_pair_delim nothing space nothing
(print_ty ~paren:false) print_ident))
args in
fprintf fmt "%s" s
| Ddecl (ty, lie) ->
let nb, ty = extract_stars ty in
assert (nb=0);
fprintf fmt "%a @[<hov>%a@];"
(print_ty ~paren:false) ty
(print_list comma (print_id_init ~stars:nb)) lie
let s = sprintf "%a @[<hov>%a@];"
(print_ty ~paren:false) ty
(print_list comma (print_id_init ~stars:nb)) lie in
fprintf fmt "%s" s
| Dstruct (s, lf) ->
fprintf fmt "struct %s@ @[<hov>{@;<1 2>@[<hov>%a@]@\n};@\n@]"
s
(print_list newline
(fun fmt (s,ty) -> fprintf fmt "%a %s;"
(print_ty ~paren:false) ty s))
lf
let s = sprintf "struct %s@ @[<hov>{@;<1 2>@[<hov>%a@]@\n};@\n@]"
s
(print_list newline
(fun fmt (s,ty) -> fprintf fmt "%a %s;"
(print_ty ~paren:false) ty s))
lf in
fprintf fmt "%s" s
| Dinclude id ->
fprintf fmt "#include<%a.h>@;" print_ident id
| Dtypedef (ty,id) ->
fprintf fmt "@[<hov>typedef@ %a@;%a;@]"
(print_ty ~paren:false) ty print_ident id
let s = sprintf "@[<hov>typedef@ %a@;%a;@]"
(print_ty ~paren:false) ty print_ident id in
fprintf fmt "%s" s
with Unprinted s -> Format.printf "Missed a def because : %s@." s
and print_body fmt (def, s) =
......@@ -927,7 +932,8 @@ module MLToC = struct
| Eraise (xs, Some r) when Sid.mem xs.xs_name env.returns ->
Debug.dprintf debug_c_extraction "RETURN@.";
expr info {env with computes_return_value = true} r
| Eraise (_, None) -> assert false (* nothing to pass to return *)
| Eraise (xs, None) when Sid.mem xs.xs_name env.returns ->
assert false (* nothing to pass to return *)
| Eraise _ -> raise (Unsupported "non break/return exception raised")
| Efor (i, sb, dir, eb, body) ->
begin match i.pv_vs.vs_ty.ty_node with
......@@ -1022,12 +1028,12 @@ module MLToC = struct
let translate_decl (info:info) (d:decl) : C.definition list
=
match d with
| Dlet (Lsym(rs, _, vl, e)) ->
if rs_ghost rs
then begin Debug.dprintf debug_c_extraction "is ghost@."; [] end
else
begin try
try
begin match d with
| Dlet (Lsym(rs, _, vl, e)) ->
if rs_ghost rs
then begin Debug.dprintf debug_c_extraction "is ghost@."; [] end
else
let params =
List.map (fun (id, ty, _gh) -> (ty_of_mlty info ty, id))
(List.filter (fun (_,_, gh) -> not gh) vl) in
......@@ -1069,24 +1075,23 @@ module MLToC = struct
let s = C.elim_nop s in
let s = C.elim_empty_blocks s in
sdecls@[C.Dfun (rs.rs_name, (rtype,params), (d,s))]
with Unsupported s ->
Format.printf "Unsupported : %s@." s; []
| Dtype [{its_name=id; its_def=idef}] ->
Debug.dprintf debug_c_extraction "PDtype %s@." id.id_string;
begin
match idef with
| Some (Dalias ty) -> [C.Dtypedef (ty_of_mlty info ty, id)]
| Some _ -> raise (Unsupported "Ddata/Drecord@.")
| None ->
begin match query_syntax info.syntax id with
| Some _ -> []
| None ->
raise (Unsupported ("type declaration without syntax or alias: "^id.id_string))
end
end
| Dtype [{its_name=id; its_def=idef}] ->
Debug.dprintf debug_c_extraction "PDtype %s@." id.id_string;
begin
match idef with
| Some (Dalias ty) -> [C.Dtypedef (ty_of_mlty info ty, id)]
| Some _ -> raise (Unsupported "Ddata/Drecord@.")
| None ->
begin match query_syntax info.syntax id with
| Some _ -> []
| None ->
raise (Unsupported ("type declaration without syntax or alias: "^id.id_string))
end
end
| _ -> [] (*TODO exn ? *)
| _ -> [] (*TODO exn ? *) end
with Unsupported s ->
Format.printf "Unsupported : %s@." s; []
let translate_decl (info:info) (d:Mltree.decl) : C.definition list
=
......@@ -1105,19 +1110,35 @@ module MLToC = struct
end
let fg ?fname m =
let name_gen suffix ?fname m =
let n = m.Pmodule.mod_theory.Theory.th_name.Ident.id_string in
match fname with
| None -> n ^ ".c"
| Some f -> f ^ "__" ^ n ^ ".c"
(*
let pr args ?old ?fname ~flat m fmt _d =
ignore(old);
let ast = Translate.translate args m in
try Print.print_file fmt args ast
with Print.Unprinted s -> (Format.printf "Could not print: %s@." s;
Format.fprintf fmt "/* Dummy file */@.")
*)
let r = match fname with
| None -> n ^ suffix
| Some f -> f ^ "__" ^ n ^ suffix in
String.lowercase_ascii r
let file_gen = name_gen ".c"
let header_gen = name_gen ".h"
let print_header_decl args ?old ?fname ~flat m fmt d =
ignore old;
ignore fname;
ignore flat;
ignore m;
ignore args;
ignore fmt;
ignore d;
() (* TODO *)
let print_prelude args ?old ?fname ~flat fmt m =
ignore old;
ignore fname;
ignore flat;
ignore args;
ignore fmt;
ignore m;
() (* TODO *)
let print_decl args ?old ?fname ~flat m fmt d =
ignore old;
ignore fname;
......@@ -1126,8 +1147,16 @@ let print_decl args ?old ?fname ~flat m fmt d =
let cds = MLToC.translate_decl args d in
List.iter (Format.fprintf fmt "%a@." Print.print_def) cds
let c_printer = Pdriver.{
desc = "printer for C code";
file_gen = file_gen;
decl_printer = print_decl;
interf_gen = Some header_gen;
interf_printer = Some print_header_decl;
prelude_printer = print_prelude }
let () =
Pdriver.register_printer "c" ~desc:"printer for C code" fg print_decl
Pdriver.register_printer "c" c_printer
(*
Local Variables:
......
src/mlw/ocaml_printer.ml
View file @ abe18efd
......@@ -693,10 +693,22 @@ let print_decl =
if not (Hashtbl.mem memo d) then begin Hashtbl.add memo d ();
Print.print_decl info fmt d end
let fg ?fname m =
let ng suffix ?fname m =
let mod_name = m.mod_theory.th_name.id_string in
let path = m.mod_theory.th_path in
(module_name ?fname path mod_name) ^ ".ml"
(module_name ?fname path mod_name) ^ suffix
let () = Pdriver.register_printer "ocaml"
~desc:"printer for OCaml code" fg print_decl
let file_gen = ng ".ml"
let mli_gen = ng ".mli"
open Pdriver
let ocaml_printer =
{ desc = "printer for Ocaml code";
file_gen = file_gen;
decl_printer = print_decl;
interf_gen = Some mli_gen;
interf_printer = None;
prelude_printer = print_empty_prelude }
let () = Pdriver.register_printer "ocaml" ocaml_printer
src/mlw/pdriver.ml
View file @ abe18efd
......@@ -229,22 +229,40 @@ let load_driver env file extra_files =
open Wstdlib
type filename_generator = ?fname:string -> Pmodule.pmodule -> string
type interface_generator = ?fname:string -> Pmodule.pmodule -> string
type printer =
type interf_printer =
printer_args -> ?old:in_channel -> ?fname:string -> flat:bool
-> Pmodule.pmodule -> Mltree.decl Pp.pp
type prelude_printer =
printer_args -> ?old:in_channel -> ?fname:string -> flat:bool
-> Pmodule.pmodule Pp.pp
let print_empty_prelude _ ?old:_ ?fname:_ ~flat:_ _ _ = ()
type decl_printer =
printer_args -> ?old:in_channel -> ?fname:string -> flat:bool ->
Pmodule.pmodule -> Mltree.decl Pp.pp
type reg_printer = Pp.formatted * filename_generator * printer
type printer =
{ desc : Pp.formatted;
file_gen : filename_generator;
decl_printer : decl_printer;
interf_gen : interface_generator option;
interf_printer : interf_printer option;
prelude_printer : prelude_printer; }
let printers : reg_printer Hstr.t = Hstr.create 17
let printers : printer Hstr.t = Hstr.create 17
exception KnownPrinter of string
exception UnknownPrinter of string
exception NoPrinter
let register_printer ~desc s fg p =
let register_printer s p =
if Hstr.mem printers s then raise (KnownPrinter s);
Hstr.replace printers s (desc, fg, p)
Hstr.replace printers s p
let lookup_printer drv =
let p = match drv.drv_printer with
......@@ -262,11 +280,11 @@ let lookup_printer drv =
}
in
try
let (_,fg,p) = Hstr.find printers p in (fg,printer_args,p)
let printer = Hstr.find printers p in printer_args, printer
with Not_found -> raise (UnknownPrinter p)
let list_printers () =
Hstr.fold (fun k (desc,_,_) acc -> (k,desc)::acc) printers []
Hstr.fold (fun k { desc = desc; _ } acc -> (k,desc)::acc) printers []
(* exception report *)
......
src/mlw/pdriver.mli
View file @ abe18efd
......@@ -39,16 +39,36 @@ val load_driver : Env.env -> string -> string list -> driver
@param string driver file name
@param string list additional drivers containing only theories/modules *)
type printer =
type filename_generator = ?fname:string -> Pmodule.pmodule -> string
type interface_generator = ?fname:string -> Pmodule.pmodule -> string
type interf_printer =
printer_args -> ?old:in_channel -> ?fname:string -> flat:bool
-> Pmodule.pmodule -> Mltree.decl Pp.pp
(** Things to do at the beginning of a module, e.g. open/#include.
Only used in modular extraction. *)
type prelude_printer =
printer_args -> ?old:in_channel -> ?fname:string -> flat:bool
-> Pmodule.pmodule Pp.pp
val print_empty_prelude: prelude_printer
type decl_printer =
printer_args -> ?old:in_channel -> ?fname:string -> flat:bool ->
Pmodule.pmodule -> Mltree.decl Pp.pp
type filename_generator = ?fname:string -> Pmodule.pmodule -> string
type printer =
{ desc : Pp.formatted;
file_gen : filename_generator;
decl_printer : decl_printer;
interf_gen : interface_generator option;
interf_printer : interf_printer option;
prelude_printer : prelude_printer; }
val register_printer :
desc:Pp.formatted -> string -> filename_generator -> printer -> unit
val register_printer : string -> printer -> unit
val lookup_printer : driver -> filename_generator * printer_args * printer
val lookup_printer : driver -> printer_args * printer
val list_printers : unit -> (string * Pp.formatted) list
......
src/tools/why3extract.ml
View file @ abe18efd
......@@ -40,6 +40,7 @@ type flat_modular = Flat | Modular
let opt_modu_flat = ref Flat
let is_uppercase = Strings.char_is_uppercase
let opt_interface = ref false
let add_opt_file x =
let invalid_path () = Format.eprintf "invalid path: %s@." x; exit 1 in
......@@ -74,6 +75,8 @@ let option_list = [
" perform a flat extraction (default option)";
"--modular", Arg.Unit (fun () -> opt_modu_flat := Modular),
" perform a modular extraction";
"--interface", Arg.Unit (fun () -> opt_interface := true),
" also extract interface files (requires modular extraction)";
"-o", Arg.String (fun s -> opt_output := Some s),
"<file|dir> destination of extracted code";
"--output", Arg.String (fun s -> opt_output := Some s),
......@@ -144,19 +147,37 @@ let print_preludes =
Printer.print_prelude fmt l
let print_mdecls ?fname m mdecls =
let (fg,pargs,pr) = Pdriver.lookup_printer opt_driver in
let pargs, printer = Pdriver.lookup_printer opt_driver in
let fg = printer.Pdriver.file_gen in
let pr = printer.Pdriver.decl_printer in
let test_decl_not_driver decl =
let decl_name = Mltree.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 flat = opt_modu_flat = Flat in
(* print interface file *)
if !opt_interface then begin
match printer.Pdriver.interf_gen, printer.Pdriver.interf_printer with
| None, _ | _, None ->
eprintf "Driver does not support interface extraction";
exit 1
| Some ig, Some ipr ->
let iout, old = get_cout_old ig m ?fname in
let ifmt = formatter_of_out_channel iout in
let pr_idecl fmt d =
fprintf fmt "%a" (ipr pargs ?old ?fname ~flat m) d in
Pp.print_list Pp.nothing pr_idecl ifmt mdecls;
if iout <> stdout then close_out iout end;
let cout, old = get_cout_old fg m ?fname in
let fmt = formatter_of_out_channel cout in
(* print driver prelude *)
let pm = pargs.Pdriver.thprelude in
print_preludes m.mod_theory.Theory.th_name fmt pm;
let flat = opt_modu_flat = Flat in
(* print module prelude *)
printer.Pdriver.prelude_printer pargs ?old ?fname ~flat fmt m;
(* print decls *)
let pr_decl fmt d = fprintf fmt "%a" (pr pargs ?old ?fname ~flat m) d in
Pp.print_list Pp.nothing pr_decl fmt mdecls;
if cout <> stdout then close_out cout end
......@@ -330,43 +351,45 @@ let () =
try
match opt_modu_flat with
| Modular -> Queue.iter do_modular opt_queue
| Flat -> let mm = Queue.fold flat_extraction Mstr.empty opt_queue in
let (_fg, pargs, pr) = Pdriver.lookup_printer opt_driver in
let cout = match opt_output with
| None -> stdout
| Some file -> open_out file in
let fmt = formatter_of_out_channel cout in
let thprelude = pargs.Pdriver.thprelude in
let print_prelude = List.iter (fun s -> fprintf fmt "%s@\n@." s) in
let rec do_preludes id =
(try
let m = find_module_id mm id in
Ident.Sid.iter do_preludes m.mod_used
with Not_found -> ());
print_preludes id fmt thprelude
in
print_prelude pargs.Pdriver.prelude;
let visit_m _ m =
do_preludes m.mod_theory.Theory.th_name;
let tm = translate_module m in
let visit_id id _ = visit ~recurs:true mm id in
Ident.Mid.iter visit_id tm.Mltree.mod_known;
in
Mstr.iter visit_m mm;
let extract fmt { info_id = id } =
let pm = find_module_id mm id in
let m = translate_module pm in
let d = Ident.Mid.find id m.Mltree.mod_known in
pr pargs ~flat:true pm fmt d in
let idl = List.rev !toextract in
let is_local { info_id = id; info_rec = r } =
let (path, m, _) = Pmodule.restore_path id in
path = [] || Mstr.mem m mm || not r in
let idl = match opt_rec_single with
| Single -> List.filter is_local idl
| Recursive -> idl in
Pp.print_list Pp.nothing extract fmt idl;
if cout <> stdout then close_out cout
| Flat ->
let mm = Queue.fold flat_extraction Mstr.empty opt_queue in
let (pargs, printer) = Pdriver.lookup_printer opt_driver in
let pr = printer.Pdriver.decl_printer in
let cout = match opt_output with
| None -> stdout
| Some file -> open_out file in
let fmt = formatter_of_out_channel cout in
let thprelude = pargs.Pdriver.thprelude in
let print_prelude = List.iter (fun s -> fprintf fmt "%s@\n@." s) in
let rec do_preludes id =
(try
let m = find_module_id mm id in
Ident.Sid.iter do_preludes m.mod_used
with Not_found -> ());
print_preludes id fmt thprelude
in
print_prelude pargs.Pdriver.prelude;
let visit_m _ m =
do_preludes m.mod_theory.Theory.th_name;
let tm = translate_module m in
let visit_id id _ = visit ~recurs:true mm id in
Ident.Mid.iter visit_id tm.Mltree.mod_known;
in
Mstr.iter visit_m mm;
let extract fmt { info_id = id } =
let pm = find_module_id mm id in
let m = translate_module pm in
let d = Ident.Mid.find id m.Mltree.mod_known in
pr pargs ~flat:true pm fmt d in
let idl = List.rev !toextract in
let is_local { info_id = id; info_rec = r } =
let (path, m, _) = Pmodule.restore_path id in
path = [] || Mstr.mem m mm || not r in
let idl = match opt_rec_single with
| Single -> List.filter is_local idl
| Recursive -> idl in
Pp.print_list Pp.nothing extract fmt idl;
if cout <> stdout then close_out cout
with e when not (Debug.test_flag Debug.stack_trace) ->
eprintf "%a@." Exn_printer.exn_printer e;
exit 1
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment