From f6acf47bfb217703fccb6dd39821668de8caa553 Mon Sep 17 00:00:00 2001
From: ploc <ploc@041b043f-8d7c-46b2-b46e-ef0dd855326e>
Date: Thu, 26 Nov 2015 17:17:51 +0000
Subject: [PATCH] Plugin based framework
---
configure.ac | 70 +++++++++++++++++++++----------
src/_tags | 1 +
src/backends/C/c_backend_main.ml | 6 +--
src/global.ml | 1 +
src/main_lustre_compiler.ml | 48 ++-------------------
src/options.ml | 5 +--
src/pluginType.ml | 17 ++++++++
src/plugins.ml | 35 ++++++++++++++--
src/{ => plugins/mpfr}/mpfr.ml | 0
src/plugins/salsa/salsa_plugin.ml | 42 +++++++++++++++++++
src/plugins/scopes/scopes.ml | 30 ++++++++++++-
11 files changed, 174 insertions(+), 81 deletions(-)
create mode 100644 src/pluginType.ml
rename src/{ => plugins/mpfr}/mpfr.ml (100%)
create mode 100644 src/plugins/salsa/salsa_plugin.ml
diff --git a/configure.ac b/configure.ac
index 0059f094..23099589 100644
--- a/configure.ac
+++ b/configure.ac
@@ -7,9 +7,24 @@ AC_SUBST(SVN_REVISION)
AC_CONFIG_SRCDIR([src/main_lustre_compiler.ml])
+AC_PATH_PROG([OCAMLC],[ocamlc],[:])
+AC_MSG_CHECKING(OCaml version)
+ocamlc_version=`$OCAMLC -v | grep version | rev| cut -d \ -f 1 | rev`
+major=`echo $ocamlc_version | cut -d . -f 1`
+minor=`echo $ocamlc_version | cut -d . -f 2`
+if (test "$major" -lt 3 -a "$minor" -lt 12 ); then
+ AC_MSG_ERROR([Ocaml version must be at least 3.12. You have version $ocamlc_version])
+fi
+AC_MSG_RESULT(valid ocaml version detected: $ocamlc_version)
+
+AC_PATH_PROG([OCAMLBUILD],[ocamlbuild],[:])
+
+
# default prefix is /usr/local
AC_PREFIX_DEFAULT(/usr/local)
+# Checking libs
+
AC_ARG_WITH([ocamlgraph-path],
[AS_HELP_STRING([--ocamlgraph-path],
[specify the path of ocamlgraph library. graph.cmxa should be in ocamlgraph-path @<:@default=$(ocamlfind query ocamlgraph)@:>@])],
@@ -23,32 +38,25 @@ AC_ARG_WITH([ocamlgraph-path],
)
AC_SUBST(OCAMLGRAPH_PATH)
-
-AC_PATH_PROG([OCAMLC],[ocamlc],[:])
-AC_MSG_CHECKING(OCaml version)
-ocamlc_version=`$OCAMLC -v | grep version | rev| cut -d \ -f 1 | rev`
-major=`echo $ocamlc_version | cut -d . -f 1`
-minor=`echo $ocamlc_version | cut -d . -f 2`
-if (test "$major" -lt 3 -a "$minor" -lt 11 ); then
- AC_MSG_ERROR([Ocaml version must be at least 3.11. You have version $ocamlc_version])
-fi
-AC_MSG_RESULT(valid ocaml version detected: $ocamlc_version)
-
-AC_PATH_PROG([OCAMLBUILD],[ocamlbuild],[:])
-
-
-# Checking libs
-
-# Checks for libraries. OCamlgraph
AC_MSG_CHECKING(ocamlgraph library)
- ocamlgraph_lib=`find $OCAMLGRAPH_PATH -iname graph.cmxa | grep -m 1 -o "graph.cmxa"`
+ ocamlgraph_lib=`find $OCAMLGRAPH_PATH -iname graph.cmxa -nowarn | grep -m 1 -o "graph.cmxa"`
if (test "x$ocamlgraph_lib" = xgraph.cmxa ); then
- ocamlgraph_lib_full=`find $OCAMLGRAPH_PATH -iname graph.cmxa | grep -m 1 "graph.cmxa"`
- AC_MSG_RESULT(library detected: $ocamlgraph_lib_full )
- else
+ ocamlgraph_lib_full=`find $OCAMLGRAPH_PATH -iname graph.cmxa -nowarn | grep -m 1 "graph.cmxa"`
+ AC_MSG_RESULT($ocamlgraph_lib_full )
+ else
AC_MSG_ERROR([ocamlgraph library not installed in $OCAMLGRAPH_PATH])
fi
+AC_CHECK_LIB(gmp, __gmpz_init,
+ [gmp=yes],
+ [AC_MSG_RESULT([GNU MP not found])
+ gmp=no])
+
+AC_CHECK_LIB(mpfr, mpfr_add, [mpfr=yes],
+ [AC_MSG_RESULT(
+[MPFR not found])
+mpfr=no])
+
# Workaround to solve an issue with ocamlbuild and C libraries.
# oCFLAGS="$CFLAGS"
@@ -86,11 +94,27 @@ AC_DEFINE_DIR([abs_datadir], [datadir])
# Instanciation
AC_CONFIG_FILES([Makefile
src/Makefile
- src/myocamlbuild.ml
+ src/myocamlbuild.ml
src/version.ml])
AC_OUTPUT
# summary
-dnl AC_MSG_NOTICE(******** Configuration ********)
+AC_MSG_NOTICE(******** Configuration ********)
+AC_MSG_NOTICE(bin path: $prefix/bin)
+AC_MSG_NOTICE(include path: $prefix/include)
+AC_MSG_NOTICE(******** Plugins ********)
+
+ if (test "x$gmp" = xyes -a "x$mpfr" = xyes ); then
+ AC_MSG_NOTICE([-mpfr option enable])
+
+ else
+ AC_MSG_WARN([MPFR option cannot be activated. Requires GMP and MPFR libs])
+
+ fi
+
+AC_MSG_NOTICE
+AC_MSG_NOTICE(******** Configuration ********)
+AC_MSG_NOTICE(******** Configuration ********)
+
diff --git a/src/_tags b/src/_tags
index e3fd0e0e..139426ce 100644
--- a/src/_tags
+++ b/src/_tags
@@ -2,6 +2,7 @@
"backends/Horn": include
"plugins/salsa": include
"plugins/scopes": include
+"plugins/mpfr": include
<**/.svn>: -traverse
<**/.svn>: not_hygienic
"main_lustre_compiler.native": use_graph
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index f17f617e..d01a9e56 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -139,10 +139,8 @@ let print_main_code fmt m =
print_main_memory_allocation mname main_mem fmt m;
print_main_initialize mname main_mem fmt m;
print_main_loop mname main_mem fmt m;
- if Scopes.Plugin.is_active () then
- begin
- fprintf fmt "@ %t" Scopes.Plugin.pp
- end;
+
+ Plugins.c_backend_main_loop_body_suffix fmt ();
fprintf fmt "@]@ }@ @ ";
print_main_clear mname main_mem fmt m;
fprintf fmt "@ return 1;";
diff --git a/src/global.ml b/src/global.ml
index 892f630c..08f09908 100644
--- a/src/global.ml
+++ b/src/global.ml
@@ -3,6 +3,7 @@ let clock_env : (Clocks.clock_expr Env.t) ref = ref Env.initial
let basename = ref ""
let main_node = ref ""
+
module TypeEnv =
struct
let lookup_value ident = Env.lookup_value !type_env ident
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 5bc03a73..ab22f4bd 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -112,7 +112,7 @@ let stage1 prog dirname basename =
in
(* Checking stateless/stateful status *)
- if Scopes.Plugin.is_active () then
+ if Plugins.check_force_stateful () then
force_stateful_decls prog
else
check_stateless_decls prog;
@@ -275,27 +275,6 @@ let stage2 prog =
in
(* Salsa optimize machine code *)
- let machine_code =
- if !Options.salsa_enabled then
- begin
- check_main ();
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization (phase 3)@ ");
- (* Selecting float constants for Salsa *)
- let constEnv = List.fold_left (
- fun accu c_topdecl ->
- match c_topdecl.top_decl_desc with
- | Const c when Types.is_real_type c.const_type ->
- (c.const_id, c.const_value) :: accu
- | _ -> accu
- ) [] (Corelang.get_consts prog)
- in
- List.map
- (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv)
- machine_code
- end
- else
- machine_code
- in
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
machine_code);
@@ -391,23 +370,8 @@ let compile_source dirname basename extension =
let machine_code =
stage2 prog
in
- if Scopes.Plugin.show_scopes () then
- begin
- let all_scopes = Scopes.compute_scopes prog !Options.main_node in
- (* Printing scopes *)
- if !Options.verbose_level >= 1 then
- Format.printf "Possible scopes are:@ ";
- Format.printf "@[<v>%a@ @]@.@?" Scopes.print_scopes all_scopes;
- exit 0
-
- end;
- let machine_code =
- if Scopes.Plugin.is_active () then
- Scopes.Plugin.process_scopes !Options.main_node prog machine_code
- else
- machine_code
- in
+ let machine_code = Plugins.refine_machine_code prog machine_code in
stage3 prog machine_code dependencies basename;
begin
@@ -443,13 +407,7 @@ let _ =
try
Printexc.record_backtrace true;
- let options = Options.options @
- List.flatten (
- List.map Options.plugin_opt [
- Scopes.Plugin.name, Scopes.Plugin.activate, Scopes.Plugin.options
- ]
- )
- in
+ let options = Options.options @ (Plugins.options ()) in
Arg.parse options anonymous usage
with
diff --git a/src/options.ml b/src/options.ml
index 99744c53..0426588b 100755
--- a/src/options.ml
+++ b/src/options.ml
@@ -41,13 +41,12 @@ let horntraces = ref false
let horn_cex = ref false
let horn_queries = ref false
-let salsa_enabled = ref false
let set_mpfr prec =
if prec > 0 then (
mpfr := true;
mpfr_prec := prec;
- salsa_enabled := false; (* We deactivate salsa *)
+ (* salsa_enabled := false; (* We deactivate salsa *) TODO *)
)
else
failwith "mpfr requires a positive integer"
@@ -69,8 +68,6 @@ let options =
"-horn-traces", Arg.Unit (fun () -> output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
"-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
"-horn-queries", Arg.Unit (fun () -> output := "horn"; horn_queries:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
- "-salsa", Arg.Set salsa_enabled, "activate Salsa optimization <default>";
- "-no-salsa", Arg.Clear salsa_enabled, "deactivate Salsa optimization";
"-print_reuse", Arg.Set print_reuse, "prints variable reuse policy";
"-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
"-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inline all node calls (require a main node). Implies constant unfolding";
diff --git a/src/pluginType.ml b/src/pluginType.ml
new file mode 100644
index 00000000..fda050a6
--- /dev/null
+++ b/src/pluginType.ml
@@ -0,0 +1,17 @@
+module type PluginType =
+sig
+ val name: string
+ val activate: unit -> unit
+ val options: (string * Arg.spec * string) list
+ val check_force_stateful : unit -> bool
+ val refine_machine_code: LustreSpec.top_decl list ->
+ Machine_code.machine_t list -> Machine_code.machine_t list
+ val c_backend_main_loop_body_suffix : Format.formatter -> unit -> unit
+end
+
+module Default =
+struct
+ let check_force_stateful () = false
+ let refine_machine_code prog machines = machines
+ let c_backend_main_loop_body_suffix fmt () = ()
+end
diff --git a/src/plugins.ml b/src/plugins.ml
index 44fccd4b..f6700914 100644
--- a/src/plugins.ml
+++ b/src/plugins.ml
@@ -1,11 +1,40 @@
open LustreSpec
-module type PluginType =
-sig
+let plugins =
+ [
+ (module Scopes.Plugin : PluginType.PluginType);
+ (module Salsa_plugin.Plugin : PluginType.PluginType)
+ ]
-end
+let options () =
+ List.flatten (
+ List.map Options.plugin_opt (
+ List.map (fun m ->
+ let module M = (val m : PluginType.PluginType) in
+ (M.name, M.activate, M.options)
+ ) plugins
+ ))
+let check_force_stateful () =
+ List.exists (fun m ->
+ let module M = (val m : PluginType.PluginType) in
+ M.check_force_stateful ()
+ ) plugins
+
+let refine_machine_code prog machine_code =
+ List.fold_left (fun accu m ->
+ let module M = (val m : PluginType.PluginType) in
+ M.refine_machine_code prog accu
+ ) machine_code plugins
+
+
+let c_backend_main_loop_body_suffix fmt () =
+ List.iter (fun (m: (module PluginType.PluginType)) ->
+ let module M = (val m : PluginType.PluginType) in
+ M.c_backend_main_loop_body_suffix fmt ()) plugins
+
+(* Specific treatment of annotations when inlining, specific of declared plugins *)
let inline_annots rename_var_fun annot_list =
List.map (
diff --git a/src/mpfr.ml b/src/plugins/mpfr/mpfr.ml
similarity index 100%
rename from src/mpfr.ml
rename to src/plugins/mpfr/mpfr.ml
diff --git a/src/plugins/salsa/salsa_plugin.ml b/src/plugins/salsa/salsa_plugin.ml
new file mode 100644
index 00000000..ca713ab9
--- /dev/null
+++ b/src/plugins/salsa/salsa_plugin.ml
@@ -0,0 +1,42 @@
+open Format
+open LustreSpec
+
+let salsa_enabled = ref false
+ (* "-salsa", Arg.Set salsa_enabled, "activate Salsa optimization <default>"; *)
+ (* "-no-salsa", Arg.Clear salsa_enabled, "deactivate Salsa optimization"; *)
+
+
+module Plugin =
+(struct
+ include PluginType.Default
+ let name = "salsa"
+
+ let options = [
+
+ ]
+
+ let activate () = salsa_enabled := true
+
+ let refine_machine_code prog machine_code =
+ if !salsa_enabled then
+ begin
+ Compiler_common.check_main ();
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization (phase 3)@ ");
+ (* Selecting float constants for Salsa *)
+ let constEnv = List.fold_left (
+ fun accu c_topdecl ->
+ match c_topdecl.top_decl_desc with
+ | Const c when Types.is_real_type c.const_type ->
+ (c.const_id, c.const_value) :: accu
+ | _ -> accu
+ ) [] (Corelang.get_consts prog)
+ in
+ List.map
+ (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv)
+ machine_code
+ end
+ else
+ machine_code
+
+
+ end: PluginType.PluginType)
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index 1f1920bd..19e5b52d 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -227,7 +227,7 @@ let update_machine machine =
}
-module Plugin =
+module Plugin : PluginType.PluginType =
struct
let name = "scopes"
let is_active () =
@@ -250,7 +250,8 @@ struct
let activate () =
option_scopes := true;
Options.optimization := 0; (* no optimization *)
- Options.salsa_enabled := false; (* No salsa *)
+
+ (* Options.salsa_enabled := false; (\* No salsa *\) TODO *)
()
let rec is_valid_path path nodename prog machines =
@@ -312,6 +313,31 @@ struct
let pp fmt = pp_scopes fmt !scopes_map
+ let check_force_stateful () = true
+
+ let refine_machine_code prog machine_code =
+ if show_scopes () then
+ begin
+ let all_scopes = compute_scopes prog !Options.main_node in
+ (* Printing scopes *)
+ if !Options.verbose_level >= 1 then
+ Format.printf "Possible scopes are:@ ";
+ Format.printf "@[<v>%a@ @]@.@?" print_scopes all_scopes;
+ exit 0
+ end;
+ if is_active () then
+ process_scopes !Options.main_node prog machine_code
+ else
+ machine_code
+
+
+
+ let c_backend_main_loop_body_suffix fmt () =
+ if is_active () then
+ begin
+ Format.fprintf fmt "@ %t" pp
+ end;
+
end
(* Local Variables: *)
--
GitLab