Commit 13ae52d0 authored by François Bobot's avatar François Bobot

Plugin inside whyconf file

parent ac73e47b
......@@ -113,7 +113,7 @@ LIBGENERATED = src/util/rc.ml src/parser/lexer.ml \
src/driver/driver_lexer.ml
LIB_UTIL = stdlib exn_printer debug pp loc print_tree \
hashweak hashcons util sysutil rc
hashweak hashcons util sysutil rc plugin
LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
......@@ -574,7 +574,7 @@ install_no_local::
# bench
########
.PHONY: bench test
.PHONY: bench test comp_bench_plugins
bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
sh bench/bench \
......@@ -585,11 +585,13 @@ BENCH_PLUGINS_CMO := helloworld.cmo
BENCH_PLUGINS_CMO := $(addprefix bench/plugins/,$(BENCH_PLUGINS_CMO))
BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)
bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
bin/why.byte -D bench/plugins/helloworld.drv \
tests/test-jcf.why -T Test -G G
bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv \
tests/test-jcf.why -T Test -G G
comp_bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS)
# bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
# bin/why.byte -D bench/plugins/helloworld.drv \
# tests/test-jcf.why -T Test -G G
# bin/why.$(OCAMLBEST) -D bench/plugins/helloworld.drv \
# tests/test-jcf.why -T Test -G G
###############
# test targets
......
......@@ -19,10 +19,10 @@
open Why
let print_context _ fmt _ = Format.fprintf fmt "helloworld@\n"
let print_context _ _ _ ?old:_ fmt _ = Format.fprintf fmt "helloworld@\n"
let transform_context = Register.identity
let transform_context = Trans.identity
let () =
Driver.register_printer "helloworld" print_context;
Driver.register_transform "helloworld" transform_context
let () =
Printer.register_printer "helloworld" print_context;
Trans.register_transform "helloworld" transform_context
......@@ -34,6 +34,10 @@ let auto = ref false
let set_oref r = (fun s -> r := Some s)
let plugins = Queue.create ()
let add_plugin x = Queue.add x plugins
let option_list = Arg.align [
(* "--libdir", Arg.String (set_oref libdir), *)
(* "<dir> set the lib directory ($WHY3LIB)"; *)
......@@ -43,10 +47,26 @@ let option_list = Arg.align [
"<file> use this configuration file, create it if it doesn't exist
($WHY_CONFIG), otherwise use the default one";
"--autodetect-provers", Arg.Set auto,
" autodetect the provers in the $PATH"]
" autodetect the provers in the $PATH";
"--install-plugin", Arg.String add_plugin,
"install a plugin to the actual libdir";
]
let anon_file _ = Arg.usage option_list usage_msg; exit 1
let install_plugin main p =
begin match Plugin.check_extension p with
| Plugin.Extbad -> eprintf "Unknown extension (.cmo|.cmxs) : %s@." p;exit 1
| Plugin.Extother ->
eprintf "This plugin %s will not be used with this kind of compilation@."
p
| Plugin.Extgood -> ()
end;
let base = Filename.basename p in
let pluginsdir = Whyconf.pluginsdir main in
Sysutil.copy_file p (Filename.concat pluginsdir base);
Whyconf.add_plugin main (Filename.chop_extension base)
let () =
Arg.parse option_list anon_file usage_msg;
let config =
......@@ -61,6 +81,7 @@ let () =
!libdir in *)
(* let main = option_apply main (fun d -> {main with datadir = d})
!datadir in *)
let main = Queue.fold install_plugin main plugins in
let config = set_main config main in
let conf_file = get_conf_file config in
let conf_file_doesnt_exist = not (Sys.file_exists conf_file) in
......
......@@ -57,6 +57,9 @@ type main = {
(* default prover memory limit in megabytes (0 unlimited)*)
running_provers_max : int;
(* max number of running prover processes *)
plugins : string list;
(* plugins to load, without extension, relative to
[private_libdir]/plugins *)
}
let libdir m =
......@@ -89,6 +92,24 @@ let running_provers_max m = m.running_provers_max
let set_limits m time mem running =
{ m with timelimit = time; memlimit = mem; running_provers_max = running }
let plugins m = m.plugins
let set_plugins m pl =
(* TODO : sanitize? *)
{ m with plugins = pl}
let add_plugin m p =
if List.mem p m.plugins
then m
else { m with plugins = List.rev (p::(List.rev m.plugins))}
let pluginsdir m = Filename.concat m.private_libdir "plugins"
let load_plugins m =
let dirs = [pluginsdir m] in
let load x =
try Plugin.load ~dirs x
with Plugin.Plugin_Not_Found _ as exn
-> Format.eprintf "%a@." Exn_printer.exn_printer exn in
List.iter load m.plugins
type config = {
conf_file : string; (* "/home/innocent_user/.why.conf" *)
config : Rc.t ;
......@@ -104,6 +125,7 @@ let default_main =
timelimit = 10;
memlimit = 0;
running_provers_max = 2;
plugins = [];
}
let set_main rc main =
......@@ -115,6 +137,7 @@ let set_main rc main =
let section = set_int section "memlimit" main.memlimit in
let section =
set_int section "running_provers_max" main.running_provers_max in
let section = set_stringl section "plugin" main.plugins in
set_section rc "main" section
let set_prover id prover family =
......@@ -158,6 +181,7 @@ let load_main dirname section =
running_provers_max =
get_int ~default:default_main.running_provers_max section
"running_provers_max";
plugins = get_stringl ~default:[] section "plugin";
}
......
......@@ -38,6 +38,11 @@ val timelimit: main -> int
val memlimit: main -> int
val running_provers_max: main -> int
val set_limits: main -> int -> int -> int -> main
val plugins : main -> string list
val pluginsdir : main -> string
val set_plugins : main -> string list -> main
val add_plugin : main -> string -> main
val load_plugins : main -> unit
type config
(** A configuration linked to an rc file. Whyconf gives access to
......
......@@ -191,8 +191,31 @@ let option_list = Arg.align [
let () =
Arg.parse option_list add_opt_file usage_msg;
(* TODO? : Since drivers can dynlink ml code they can add printer,
transformations, ... So drivers should be loaded before listing *)
(** Debug flag *)
if !opt_debug_all then begin
List.iter (fun (_,f,_) -> Debug.set_flag f) (Debug.list_flags ());
Debug.unset_flag Typing.debug_parse_only;
Debug.unset_flag Typing.debug_type_only
end;
List.iter (fun s -> Debug.set_flag (Debug.lookup_flag s)) !opt_debug;
if !opt_parse_only then Debug.set_flag Typing.debug_parse_only;
if !opt_type_only then Debug.set_flag Typing.debug_type_only;
(** Configuration *)
let config = try read_config !opt_config with Not_found ->
option_iter (eprintf "Config file '%s' not found.@.") !opt_config;
option_iter
(eprintf "No config file found (required by '-P %s').@.") !opt_prover;
exit 1;
in
let main = get_main config in
Whyconf.load_plugins main;
(** listings*)
let opt_list = ref false in
if !opt_list_transforms then begin
opt_list := true;
......@@ -276,25 +299,6 @@ let () =
opt_print_theory := true
end;
if !opt_debug_all then begin
List.iter (fun (_,f,_) -> Debug.set_flag f) (Debug.list_flags ());
Debug.unset_flag Typing.debug_parse_only;
Debug.unset_flag Typing.debug_type_only
end;
List.iter (fun s -> Debug.set_flag (Debug.lookup_flag s)) !opt_debug;
if !opt_parse_only then Debug.set_flag Typing.debug_parse_only;
if !opt_type_only then Debug.set_flag Typing.debug_type_only;
let config = try read_config !opt_config with Not_found ->
option_iter (eprintf "Config file '%s' not found.@.") !opt_config;
option_iter
(eprintf "No config file found (required by '-P %s').@.") !opt_prover;
exit 1;
in
let main = get_main config in
opt_loadpath := List.rev_append !opt_loadpath (Whyconf.loadpath main);
if !opt_timelimit = None then opt_timelimit := Some (Whyconf.timelimit main);
if !opt_memlimit = None then opt_memlimit := Some (Whyconf.memlimit main);
......
open Config
type plugin = string
let debug = Debug.register_flag "load_plugin"
exception Plugin_Not_Found of plugin * string list
let add_extension p =
if Dynlink.is_native then p^".cmxs" else p^".cmo"
let load ?dirs p =
let p = add_extension p in
let f = match dirs with
| None -> p
| Some ld ->
let rec find = function
| [] -> raise (Plugin_Not_Found (p,ld))
| d::ld ->
let f = Filename.concat d p in
if Sys.file_exists f then f else find ld in
find ld in
Debug.dprintf debug "Plugin loaded : %s" f;
Dynlink.loadfile_private f
type ext =
(* not a plugin extension *)
| Extbad
(* good plugin extension *)
| Extgood
(* good plugin extension but not the current compilation used *)
| Extother
let check_extension f =
let cmxs = Filename.check_suffix f ".cmxs" in
let cmo = Filename.check_suffix f ".cmo" in
if not cmxs && not cmo
then Extbad
else
if (if Dynlink.is_native then cmxs else cmo)
then Extgood else Extother
let () =
Exn_printer.register (fun fmt exn ->
match exn with
| Plugin_Not_Found (pl,sl) ->
Format.fprintf fmt "The plugin %s can't be found in the directories %a"
pl (Pp.print_list Pp.space Pp.string) sl
| _ -> raise exn)
type plugin = string
exception Plugin_Not_Found of plugin * string list
val debug : Debug.flag
(** debug flag for the plugin mechanism (option "--debug
load_plugin")
If set [load_plugin] prints on stderr exactly which plugin are loaded.
*)
val load : ?dirs:string list -> plugin -> unit
(* [load_plugin ~dir plugin] looks in the directories [dir] for the
plugin named [plugin]. It add the extension .cmo or .cmxs to the
filename according to the compilation used for the main program *)
type ext =
(* not a plugin extension *)
| Extbad
(* good plugin extension *)
| Extgood
(* good plugin extension but not the current compilation used *)
| Extother
val check_extension : plugin -> ext
......@@ -106,3 +106,11 @@ let call_asynchronous (f : unit -> 'a) =
| _ -> raise (Bad_execution ps) in
f
let copy_file from to_ =
let cin = open_in from in
let cout = open_out to_ in
let buff = String.make 1024 ' ' in
let n = ref 0 in
while n := input cin buff 0 1024; !n <> 0 do
output cout buff 0 !n
done
......@@ -55,3 +55,6 @@ val call_asynchronous : (unit -> 'a) -> (unit -> 'a)
it is not as bad as it can be in 3.11.0 :
http://caml.inria.fr/mantis/view.php?id=4577
*)
val copy_file : string -> string -> unit
(** [copy_file from to] copy the file from [from] to [to] *)
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