Optional compilation of Controllable-Nbac-related modules and tools.

This commit is contained in:
Nicolas Berthier 2014-10-21 15:24:48 +02:00
parent 3b27de8146
commit 541dd83fca
10 changed files with 1232 additions and 15 deletions

1
.gitignore vendored
View File

@ -30,5 +30,6 @@ lib/java/.classpath
/test/image_filters/java/* /test/image_filters/java/*
compiler/doc.odocl compiler/doc.odocl
compiler/doc.docdir compiler/doc.docdir
compiler/_tags
config config
config.status config.status

View File

@ -1,9 +1,13 @@
include ../config include ../config
ifeq ($(ENABLE_SIMULATOR), yes)
BIN:=heptc.$(TARGET) hepts.$(TARGET)
else
BIN:=heptc.$(TARGET) BIN:=heptc.$(TARGET)
ifeq ($(ENABLE_SIMULATOR), yes)
BIN:=$(BIN) hepts.$(TARGET)
endif
ifeq ($(ENABLE_CTRL2EPT), yes)
BIN:=$(BIN) ctrl2ept.$(TARGET)
endif endif
.PHONY: all clean native byte clean debug install .PHONY: all clean native byte clean debug install

View File

@ -1,8 +1,11 @@
<global> or <utilities> or <minils> or <heptagon> or <main> or <obc>:include <global> or <utilities> or <minils> or <heptagon> or <main> or <obc>:include
<**/*.ml*>: debug, dtypes, package(ocamlgraph), package(reatk.ctrlNbac) <**/*.ml*>: debug, dtypes, package(ocamlgraph)
<preproc.ml>: camlp4of, package(camlp4) <preproc.ml>: camlp4of, package(camlp4)
true: use_menhir true: use_menhir
<**/*.{byte,native}>: package(unix), package(str), debug, custom <**/*.{byte,native}>: package(unix), package(str), debug, custom
<**/heptc.{byte,native}>: package(menhirLib), package(ocamlgraph), package(reatk.ctrlNbac) <**/heptc.{byte,native}>: package(menhirLib), package(ocamlgraph)
<main/hepts.{ml,byte,native}>: package(lablgtk2), thread <main/hepts.{ml,byte,native}>: package(lablgtk2), thread
<**/*.ml*> or <**/heptc.{byte,native}>: @package_reatk_ctrlNbac@
"minils/main/mls_compiler.ml" or "main/mls2seq.ml": pp(camlp4o pa_macro.cmo @ctrln_pp@)

View File

@ -38,6 +38,7 @@ type program_target =
| Obc_no_params of (Obc.program -> unit) | Obc_no_params of (Obc.program -> unit)
| Minils of (Minils.program -> unit) | Minils of (Minils.program -> unit)
| Minils_no_params of (Minils.program -> unit) | Minils_no_params of (Minils.program -> unit)
| Disabled_target
type interface_target = type interface_target =
| IObc of (Obc.interface -> unit) | IObc of (Obc.interface -> unit)
@ -76,15 +77,23 @@ let java_conf () =
Compiler_options.do_scalarize := true; Compiler_options.do_scalarize := true;
() ()
;; IFDEF ENABLE_CTRLN THEN
let ctrln_targets =
[ mk_target "ctrln" (Minils_no_params ignore) ]
;; ELSE
let ctrln_targets =
[ mk_target "ctrln" Disabled_target ]
;; ENDIF
let targets = let targets =
[ mk_target ~interface:(IObc Cmain.interface) "c" (Obc_no_params Cmain.program); [ mk_target ~interface:(IObc Cmain.interface) "c" (Obc_no_params Cmain.program);
mk_target ~load_conf:java_conf "java" (Obc Java_main.program); mk_target ~load_conf:java_conf "java" (Obc Java_main.program);
mk_target ~load_conf:java_conf "java14" (Obc Java14_main.program); mk_target ~load_conf:java_conf "java14" (Obc Java14_main.program);
mk_target "z3z" (Minils_no_params ignore); mk_target "z3z" (Minils_no_params ignore);
mk_target "ctrln" (Minils_no_params ignore); (* NB: `ignore'? *)
mk_target "obc" (Obc write_obc_file); mk_target "obc" (Obc write_obc_file);
mk_target "obc_np" (Obc_no_params write_obc_file); mk_target "obc_np" (Obc_no_params write_obc_file);
mk_target "epo" (Minils write_object_file) ] mk_target "epo" (Minils write_object_file) ]
@ ctrln_targets
let find_target s = let find_target s =
try try
@ -98,11 +107,11 @@ let generate_target p s =
comment "Unfolding"; comment "Unfolding";
if !Compiler_options.verbose if !Compiler_options.verbose
then List.iter (Mls_printer.print stderr) p_list in*) then List.iter (Mls_printer.print stderr) p_list in*)
let target = (find_target s).t_program in let { t_program = program; t_name = name } = find_target s in
let callgraph p = do_silent_pass "Callgraph" Callgraph.program p in let callgraph p = do_silent_pass "Callgraph" Callgraph.program p in
let mls2obc p = do_silent_pass "Translation into MiniLS" Mls2obc.program p in let mls2obc p = do_silent_pass "Translation into MiniLS" Mls2obc.program p in
let mls2obc_list p_l = do_silent_pass "Translation into MiniLS" (List.map Mls2obc.program) p_l in let mls2obc_list p_l = do_silent_pass "Translation into MiniLS" (List.map Mls2obc.program) p_l in
match target with match program with
| Minils convert_fun -> | Minils convert_fun ->
do_silent_pass "Code generation from MiniLS" convert_fun p do_silent_pass "Code generation from MiniLS" convert_fun p
| Obc convert_fun -> | Obc convert_fun ->
@ -117,6 +126,8 @@ let generate_target p s =
let o_list = mls2obc_list p_list in let o_list = mls2obc_list p_list in
let o_list = List.map Obc_compiler.compile_program o_list in let o_list = List.map Obc_compiler.compile_program o_list in
do_silent_pass "Code generation from Obc (w/o params)" List.iter convert_fun o_list do_silent_pass "Code generation from Obc (w/o params)" List.iter convert_fun o_list
| Disabled_target ->
warn "ignoring unavailable target `%s'." name
let generate_interface i s = let generate_interface i s =
let target = (find_target s).t_interface in let target = (find_target s).t_interface in

View File

@ -1 +0,0 @@
<interference.ml>:use_ocamlgraph

View File

@ -31,6 +31,8 @@ open Compiler_options
let pp p = if !verbose then Mls_printer.print stdout p let pp p = if !verbose then Mls_printer.print stdout p
;; IFDEF HAS_CTRLNBAC THEN
(* NB: I localize file name determination logics for CtrlNbac output into this (* NB: I localize file name determination logics for CtrlNbac output into this
module, because its place is not in CtrlNbacGen... *) module, because its place is not in CtrlNbacGen... *)
(** [gen_n_output_ctrln p] translates the Minils program [p] into (** [gen_n_output_ctrln p] translates the Minils program [p] into
@ -49,6 +51,17 @@ let gen_n_output_ctrln p =
end nodes; end nodes;
p p
let maybe_ctrln_pass p =
let ctrln = List.mem "ctrln" !target_languages in
let _p = pass "Controllable Nbac generation" ctrln gen_n_output_ctrln p pp in
()
;; ELSE
let maybe_ctrln_pass p = p
;; END
let compile_program p = let compile_program p =
(* Clocking *) (* Clocking *)
let p = let p =
@ -88,8 +101,7 @@ let compile_program p =
pass "Scheduling" true Schedule.program p pp pass "Scheduling" true Schedule.program p pp
in in
let ctrln = List.mem "ctrln" !target_languages in let _p = maybe_ctrln_pass p in
let _p = pass "Controllable Nbac generation" ctrln gen_n_output_ctrln p pp in
(* NB: XXX _p is ignored for now... *) (* NB: XXX _p is ignored for now... *)
let z3z = List.mem "z3z" !target_languages in let z3z = List.mem "z3z" !target_languages in

View File

@ -59,6 +59,10 @@ let separateur = "\n*********************************************\
let comment ?(sep=separateur) s = let comment ?(sep=separateur) s =
if !verbose then Format.printf "%s%s@." sep s if !verbose then Format.printf "%s%s@." sep s
let warn: ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a = fun f ->
Format.kfprintf (fun f -> Format.kfprintf (fun f -> Format.pp_print_newline f ()) f)
Format.std_formatter "Warning: " f
let do_pass d f p pp = let do_pass d f p pp =
comment (d ^ " ...\n"); comment (d ^ " ...\n");
let _start = Unix.gettimeofday () in let _start = Unix.gettimeofday () in

View File

@ -1 +0,0 @@
<interference_graph.ml>: use_ocamlgraph

1179
configure vendored

File diff suppressed because it is too large Load Diff

View File

@ -61,7 +61,12 @@ AC_CHECK_OCAML_PKG([lablgtk2])
AC_CHECK_OCAML_PKG([reatk.ctrlNbac]) AC_CHECK_OCAML_PKG([reatk.ctrlNbac])
if test "${OCAML_PKG_reatk_ctrlNbac}" = "no"; then if test "${OCAML_PKG_reatk_ctrlNbac}" = "no"; then
AC_MSG_ERROR([Please install reatk package.]) package_reatk_ctrlNbac="ocaml"; #dummy flag
ctrln_pp="-UENABLE_CTRLN"
AC_MSG_WARN([Controllable-Nbac backend and translators disabled.])
else
package_reatk_ctrlNbac="package(reatk.ctrlNbac)"
ctrln_pp="-DENABLE_CTRLN"
fi fi
if test "$enable_local_stdlib" = "yes"; then if test "$enable_local_stdlib" = "yes"; then
@ -77,3 +82,7 @@ AC_SUBST(stdlib_dir)
AC_SUBST(enable_simulator) AC_SUBST(enable_simulator)
AC_OUTPUT(config) AC_OUTPUT(config)
AC_SUBST(package_reatk_ctrlNbac)
AC_SUBST(ctrln_pp)
AC_OUTPUT(compiler/_tags)