diff --git a/src/_tags b/src/_tags
index 83271a255dab735f641d89cb6f23464ae9bd478f..34882487d41ffcacb3a894b58da09f0d1e7c750a 100644
--- a/src/_tags
+++ b/src/_tags
@@ -8,15 +8,11 @@
"main_lustre_compiler.native": package(ocamlgraph)
"main_lustre_compiler.native": use_str
"main_lustre_compiler.native": use_unix
-<<<<<<< HEAD
-<*.ml{,i}>: package(ocamlgraph)
-<*.ml{,i}>: use_str
-<*.ml{,i}>: use_unix
-=======
"main_lustre_compiler.native": use_num, package(salsa)
+
+#<*.ml{,i}>: package(ocamlgraph)
#<*.ml{,i}>: package(salsa)
<**/*.cm?>: use_graph
#<*.ml{,i}>: use_str
#<*.ml{,i}>: use_unix
<**/*.cm?>: package(salsa)
->>>>>>> salsa
diff --git a/src/backends/Horn/horn_backend.ml b/src/backends/Horn/horn_backend.ml
index fdaac42347f56e6860234f20f0b00264b5d167e1..7995f70391daf4e6938d25d39baa2458c448e99b 100644
--- a/src/backends/Horn/horn_backend.ml
+++ b/src/backends/Horn/horn_backend.ml
@@ -27,13 +27,13 @@ open Horn_backend_collecting_sem
(*
TODO:
- gerer les traces. Ca merde pour l'instant dans le calcul des memoires sur les arrows
-
-<<<<<<< HEAD
- gerer le reset --- DONE
- reconstruire les rechable states DONE
- reintroduire le cex/traces ... DONE
- traiter les types enum et les branchements sur ces types enum (en particulier les traitements des resets qui ont lieu dans certaines branches et pas dans d'autres )
*)
+
+(************************************************
=======
(* Used to print boolean constants *)
let pp_horn_tag fmt t =
@@ -445,8 +445,8 @@ let get_cex machines fmt node machine =
;
Format.fprintf fmt "(query CEXTRACE)@."
->>>>>>> salsa
+************************************)
let main_print machines fmt =
if !Options.main_node <> "" then
begin
diff --git a/src/backends/Horn/horn_backend_collecting_sem.ml b/src/backends/Horn/horn_backend_collecting_sem.ml
index f6393bcb9ab19956f9b472bfbf5424e4daf5189c..e401527c2c29c4607d1bdde9c63c9a13917bf690 100644
--- a/src/backends/Horn/horn_backend_collecting_sem.ml
+++ b/src/backends/Horn/horn_backend_collecting_sem.ml
@@ -92,7 +92,7 @@ let check_prop machines fmt node machine =
(pp_conj (pp_horn_var machine)) main_output
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
;
- if !Options.horn_query then fprintf fmt "(query ERR)@."
+ if !Options.horn_queries then fprintf fmt "(query ERR)@."
let cex_computation machines fmt node machine =
diff --git a/src/backends/Horn/horn_backend_printers.ml b/src/backends/Horn/horn_backend_printers.ml
index a66504ecd1b3a8b6defef059cc010e9eddf233cb..f1014c5fd84be60268cdd5dd91574a82e217c577 100644
--- a/src/backends/Horn/horn_backend_printers.ml
+++ b/src/backends/Horn/horn_backend_printers.ml
@@ -42,8 +42,8 @@ let pp_horn_tag fmt t =
let rec pp_horn_const fmt c =
match c with
| Const_int i -> pp_print_int fmt i
- | Const_real r -> pp_print_string fmt r
- | Const_float r -> pp_print_float fmt r
+ | Const_real (c,e,s) -> assert false (* TODO rational pp_print_string fmt r *)
+ (* | Const_float r -> pp_print_float fmt r *)
| Const_tag t -> pp_horn_tag fmt t
| _ -> assert false
@@ -52,7 +52,7 @@ let rec pp_horn_const fmt c =
but an offset suffix may be added for array variables
*)
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
- match v with
+ match v.value_desc with
| Cst c -> pp_horn_const fmt c
| Array _
| Access _ -> assert false (* no arrays *)
@@ -66,7 +66,7 @@ let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
(* Prints a [value] indexed by the suffix list [loop_vars] *)
let rec pp_value_suffix self pp_value fmt value =
- match value with
+ match value.value_desc with
| Fun (n, vl) ->
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
| _ ->
@@ -157,7 +157,7 @@ let pp_instance_call machines reset_instances m fmt i inputs outputs =
| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
fprintf fmt "@[<v 5>(and ";
fprintf fmt "(= %a (ite %a %a %a))"
- (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (LocalVar o) (* output var *)
+ (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
(pp_horn_var m) mem_m
(pp_horn_val self (pp_horn_var m)) i1
(pp_horn_val self (pp_horn_var m)) i2
@@ -173,7 +173,7 @@ let pp_instance_call machines reset_instances m fmt i inputs outputs =
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
(Utils.pp_final_char_if_non_empty "@ " inputs)
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
- (List.map (fun v -> LocalVar v) outputs)
+ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
(Utils.pp_final_char_if_non_empty "@ " outputs)
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
@@ -187,7 +187,7 @@ let pp_instance_call machines reset_instances m fmt i inputs outputs =
inputs
(Utils.pp_final_char_if_non_empty "@ " inputs)
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
- (List.map (fun v -> LocalVar v) outputs)
+ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
)
@@ -203,14 +203,14 @@ let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ide
| MLocalAssign (i,v) ->
pp_assign
m (pp_horn_var m) fmt
- i.var_type (LocalVar i) v;
+ i.var_type (mk_val (LocalVar i) i.var_type) v;
reset_instances
| MStateAssign (i,v) ->
pp_assign
m (pp_horn_var m) fmt
- i.var_type (StateVar i) v;
+ i.var_type (mk_val (StateVar i) i.var_type) v;
reset_instances
- | MStep ([i0], i, vl) when Basic_library.is_internal_fun i ->
+ | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type) ->
assert false (* This should not happen anymore *)
| MStep (il, i, vl) ->
(* if reset instance, just print the call over mem_m , otherwise declare mem_m =
diff --git a/src/lustreSpec.ml b/src/lustreSpec.ml
index ae2524cda66d3e9c19b92b4fb656c2f00f2fa97f..8d3f73451ae937bd86f5d65ef1e5c97009fa3798 100644
--- a/src/lustreSpec.ml
+++ b/src/lustreSpec.ml
@@ -240,6 +240,7 @@ type instr_t =
| MLocalAssign of var_decl * value_t
| MStateAssign of var_decl * value_t
| MReset of ident
+ | MNoReset of ident (* used to symmetrize the reset function *)
| MStep of var_decl list * ident * value_t list
| MBranch of value_t * (label * instr_t list) list
| MComment of string
diff --git a/src/machine_code.ml b/src/machine_code.ml
index c462d8fc5a275a1b291b8fefa202f105136b54e7..25b6a0c1123055b0d32b91ceee596711cfc0e5e6 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -20,26 +20,7 @@ module OrdVarDecl:Map.OrderedType with type t=var_decl =
struct type t = var_decl;; let compare = compare end
-<<<<<<< HEAD
-type value_t =
- | Cst of constant
- | LocalVar of var_decl
- | StateVar of var_decl
- | Fun of ident * value_t list
- | Array of value_t list
- | Access of value_t * value_t
- | Power of value_t * value_t
-
-type instr_t =
- | MLocalAssign of var_decl * value_t
- | MStateAssign of var_decl * value_t
- | MReset of ident
- | MNoReset of ident (* used to symmetrize the reset function *)
- | MStep of var_decl list * ident * value_t list
- | MBranch of value_t * (label * instr_t list) list
-=======
module ISet = Set.Make(OrdVarDecl)
->>>>>>> salsa
let rec pp_val fmt v =
@@ -315,60 +296,6 @@ let specialize_op expr =
| "C" -> specialize_to_c expr
| _ -> expr
-<<<<<<< HEAD
-let rec merge_to_ite g hl =
- let loc = Location.dummy_loc in
- let mkcst x = mkexpr loc (Expr_const (Const_tag x)) in
- let g_expr = mkcst g in
- match hl with
- | [] -> assert false
- | [_, e] -> e
- | (l_c,l_e)::tl ->
- let cond_expr =
- mkpredef_call loc "=" [g_expr; mkcst l_c]
- in
- mkexpr loc (Expr_ite (cond_expr, l_e, merge_to_ite g tl))
-
-let rec translate_expr ?(ite=false) node ((m, si, j, d, s) as args) expr =
- let expr = specialize_op expr in
- match expr.expr_desc with
- | Expr_const v -> Cst v
- | Expr_ident x -> translate_ident node args x
- | Expr_array el -> Array (List.map (translate_expr node args) el)
- | Expr_access (t, i) -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
- | Expr_power (e, n) -> Power (translate_expr node args e, translate_expr node args (expr_of_dimension n))
- | Expr_tuple _
- | Expr_arrow _
- | Expr_fby _
- | Expr_pre _ -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
- | Expr_when (e1, _, _) -> translate_expr node args e1
- | Expr_merge (g, hl) -> (
- (* (\* Special treatment for functional backends. Is transformed into Ite *\) *)
- (* match !Options.output with *)
- (* | "horn" -> translate_expr node args (merge_to_ite g hl) *)
- (* | ("C" | "java") -> raise NormalizationError (\* should have been replaced by MBranch *\) *)
- (* | _ -> *)
- (Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
-
- )
-
- | Expr_appl (id, e, _) when Basic_library.is_internal_fun id ->
- let nd = node_from_name id in
- Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
- | Expr_ite (g,t,e) -> (
- (* special treatment depending on the active backend. For horn backend, ite
- are preserved in expression. While they are removed for C or Java
- backends. *)
- match !Options.output with
- | "horn" ->
- Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
- | ("C" | "java") when ite ->
- Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
- | _ ->
- (Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
- )
- | _ -> raise NormalizationError
-=======
let rec translate_expr node ((m, si, j, d, s) as args) expr =
let expr = specialize_op expr in
let value_desc =
@@ -399,7 +326,6 @@ let rec translate_expr node ((m, si, j, d, s) as args) expr =
| _ -> raise NormalizationError
in
mk_val value_desc expr.expr_type
->>>>>>> salsa
let translate_guard node args expr =
match expr.expr_desc with
@@ -470,37 +396,7 @@ let translate_eq node ((m, si, j, d, s) as args) eq =
then []
else reset_instance node args o r call_ck) @
(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
-(*
- (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
- are preserved. While they are replaced as if g then x = t else x = e in C or Java
- backends. *)
-<<<<<<< HEAD
- | [x], Expr_ite _
- (* similar treatment for merge, avoid generating MBranch instructions when using Horn backend *)
- | [x], Expr_merge _
- when (match !Options.output with | "horn" -> false (* TODO 16/12 was true *) | "C" | "java" | _ -> false)
-
- (* Remark for Ocaml: the when is shared among the two patterns *)
- ->
-=======
- | [x], Expr_ite (c, t, e)
- when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)
- ->
->>>>>>> salsa
- let var_x = get_node_var x node in
- (m,
- si,
- j,
- d,
- (control_on_clock node args eq.eq_rhs.expr_clock
- (MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
- )
-<<<<<<< HEAD
-*)
-=======
-
->>>>>>> salsa
| [x], _ -> (
let var_x = get_node_var x node in
(m, si, j, d,
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 64ebf61e0b03c365a64d050a7b26c4e4fe714246..4f3062addea5e2b483f581085c0107cc4431810d 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -1,4 +1,3 @@
-<<<<<<< HEAD
(********************************************************************)
(* *)
(* The LustreC compiler toolset / The LustreC Development Team *)
@@ -16,8 +15,10 @@ open Log
open Utils
open LustreSpec
open Compiler_common
+
+exception StopPhase1 of program
-let usage = "Usage: lustrec [options] <source-file>"
+let usage = "Usage: lustrec [options] \x1b[4msource-file\x1b[0m"
let extensions = [".ec"; ".lus"; ".lusi"]
@@ -35,7 +36,7 @@ let print_lusi prog dirname basename extension =
end
(* compile a .lusi header file *)
-let compile_header dirname basename extension =
+let compile_header dirname basename extension =
let destname = !Options.dest_dir ^ "/" ^ basename in
let header_name = basename ^ extension in
let lusic_ext = extension ^ "c" in
@@ -71,7 +72,7 @@ let compile_source_to_header prog computed_types_env computed_clocks_env dirname
begin
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
- (*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
+(*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
Lusic.print_lusic_to_h destname lusic_ext
end
else
@@ -92,15 +93,9 @@ let functional_backend () =
| "horn" | "lustre" | "acsl" -> true
| _ -> false
-(* compile a .lus source file *)
-let rec compile_source dirname basename extension =
-
- Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
-
- (* Parsing source *)
- let prog = parse_source (dirname ^ "/" ^ basename ^ extension) in
-
- (* Removing automata *)
+(* From prog to prog *)
+let stage1 prog dirname basename =
+ (* Removing automata *)
let prog = Automata.expand_decls prog in
(* Importing source *)
@@ -123,7 +118,10 @@ let rec compile_source dirname basename extension =
in
(* Checking stateless/stateful status *)
- check_stateless_decls prog;
+ if Plugins.check_force_stateful () then
+ force_stateful_decls prog
+ else
+ check_stateless_decls prog;
(* Typing *)
let computed_types_env = type_decls type_env prog in
@@ -133,13 +131,9 @@ let rec compile_source dirname basename extension =
(* Generating a .lusi header file only *)
if !Options.lusi then
- begin
- let lusi_ext = extension ^ "i" in
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@," (dirname ^ "/" ^ basename ^ lusi_ext));
- print_lusi prog dirname basename lusi_ext;
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
- exit 0
- end;
+ (* We stop here the processing and produce the current prog. It will be
+ exported as a lusi *)
+ raise (StopPhase1 prog);
(* Delay calculus *)
(* TO BE DONE LATER (Xavier)
@@ -162,13 +156,8 @@ let rec compile_source dirname basename extension =
(* Compatibility with Lusi *)
(* Checking the existence of a lusi (Lustre Interface file) *)
- (match !Options.output with
- "C" ->
- begin
- let extension = ".lusi" in
- compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
- end
- |_ -> ());
+ let extension = ".lusi" in
+ compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
Typing.uneval_prog_generics prog;
Clock_calculus.uneval_prog_generics prog;
@@ -188,11 +177,23 @@ let rec compile_source dirname basename extension =
orig prog type_env clock_env
end;
-(*Format.eprintf "Inliner.global_inline<<@.%a@.>>@." Printers.pp_prog prog;*)
(* Computes and stores generic calls for each node,
only useful for ANSI C90 compliant generic node compilation *)
if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
- (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with Corelang.Node nd -> Format.eprintf "%s calls %a" id Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
+ (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with
+ Corelang.Node nd -> Format.eprintf "%s calls %a" id
+ Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
+
+ (* Optimization of prog:
+ - Unfold consts
+ - eliminate trivial expressions
+ *)
+ let prog =
+ if !Options.const_unfold || !Options.optimization >= 4 then
+ Optimize_prog.prog_unfold_consts prog
+ else
+ prog
+ in
(* Normalization phase *)
Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
@@ -200,8 +201,22 @@ let rec compile_source dirname basename extension =
if !Options.output = "lustre" then
Normalization.unfold_arrow_active := false;
let prog = Normalization.normalize_prog prog in
+ Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
+ let prog =
+ if !Options.mpfr
+ then
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
+ Mpfr.inject_prog prog
+ end
+ else
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping FP numbers@,");
+ prog
+ end in
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
+
(* Checking array accesses *)
if !Options.check then
begin
@@ -209,18 +224,26 @@ let rec compile_source dirname basename extension =
Access.check_prog prog;
end;
+ prog, dependencies
+
+(* prog -> machine *)
+
+let stage2 prog =
+
(* Computation of node equation scheduling. It also breaks dependency cycles
and warns about unused input or memory variables *)
Log.report ~level:1 (fun fmt -> fprintf fmt ".. scheduling@,");
let prog, node_schs = Scheduling.schedule_prog prog in
- Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_warning_unused node_schs);
+ Log.report ~level:1 (fun fmt -> fprintf fmt "%a" Scheduling.pp_warning_unused node_schs);
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
+ Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
(* Optimization of prog:
- Unfold consts
- eliminate trivial expressions
+ TODO (PL): should we keep this phase or just remove it
*)
let prog =
if !Options.optimization >= 5 then
@@ -231,15 +254,24 @@ let rec compile_source dirname basename extension =
else
prog
in
+
+ (* TODO Salsa optimize prog:
+ - emits warning for programs with pre inside expressions
+ - make sure each node arguments and memory is bounded by a local annotation
+ - introduce fresh local variables for each real pure subexpression
+ *)
+ (* let prog = *)
+ (* if true then *)
+ (* Salsa.Prog.normalize prog *)
+ (* else *)
+ (* prog *)
+ (* in *)
+
(* DFS with modular code generation *)
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@ ");
let machine_code = Machine_code.translate_prog prog node_schs in
- Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
- (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
- machine_code);
-
- (* Optimize machine code *)
+ (* Optimize machine code *)
let machine_code =
if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
begin
@@ -250,45 +282,46 @@ let rec compile_source dirname basename extension =
else
machine_code
in
-
+
(* Optimize machine code *)
- let machine_code =
- if !Options.optimization >= 2 (* && !Options.output <> "horn" *) then
+ let machine_code, removed_table =
+ if !Options.optimization >= 2 (*&& !Options.output <> "horn"*) then
begin
- Log.report ~level:1
- (fun fmt -> fprintf fmt
- ".. machines optimization: const. inlining (partial eval. with const)@,");
+ Log.report ~level:1 (fun fmt -> fprintf fmt
+ ".. machines optimization: const. inlining (partial eval. with const)@,");
Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code
end
else
- machine_code
- in
+ machine_code, IMap.empty
+ in
(* Optimize machine code *)
- let machine_code = (* TODO reactivate. I disabled it because output variables were removed *)
+ let machine_code = (* TODO reactivate. I disabled it because output variables were removed *)
if false && !Options.optimization >= 3 && not (functional_backend ()) then
begin
- Log.report ~level:1
- (fun fmt -> fprintf fmt ".. machines optimization: minimize heap alloc by reusing vars@,");
- Optimize_machine.machines_fusion
- (Optimize_machine.machines_reuse_variables machine_code node_schs)
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize heap alloc by reusing vars@,");
+ let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in
+ let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
+ Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables)
end
else
machine_code
in
+
+ (* Salsa optimize machine code *)
+ Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
+ (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
+ machine_code);
+
+ machine_code
- if !Options.optimization >= 2 then
- begin
- Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
- (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
- machine_code);
- end;
+let stage3 prog machine_code dependencies basename =
(* Printing code *)
let basename = Filename.basename basename in
let destname = !Options.dest_dir ^ "/" ^ basename in
- let _ = match !Options.output with
- | "C" ->
- begin
+ match !Options.output with
+ "C" ->
+ begin
let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
let source_lib_file = destname ^ ".c" in (* Could be changed *)
let source_main_file = destname ^ "_main.c" in (* Could be changed *)
@@ -316,7 +349,7 @@ let rec compile_source dirname basename extension =
Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
(* Tracability file if option is activated *)
- if !Options.traces then (
+ if !Options.horntraces then (
let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
let traces_out = open_out traces_file in
let fmt = formatter_of_out_channel traces_out in
@@ -335,10 +368,48 @@ let rec compile_source dirname basename extension =
end
| _ -> assert false
+
+(* compile a .lus source file *)
+let compile_source dirname basename extension =
+
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
+
+ (* Parsing source *)
+ let prog = parse_source (dirname ^ "/" ^ basename ^ extension) in
+
+ let prog =
+ if !Options.mpfr then
+ Mpfr.mpfr_module::prog
+ else
+ prog
in
+ let prog, dependencies =
+ try
+ stage1 prog dirname basename
+ with StopPhase1 prog -> (
+ if !Options.lusi then
+ begin
+ let lusi_ext = ".lusi" (* extension ^ "i" *) in
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@," (dirname ^ "/" ^ basename ^ lusi_ext));
+ print_lusi prog dirname basename lusi_ext;
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
+ exit 0
+ end
+ else
+ assert false
+ )
+ in
+
+ let machine_code =
+ stage2 prog
+ in
+
+ let machine_code = Plugins.refine_machine_code prog machine_code in
+
+ stage3 prog machine_code dependencies basename;
begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
- (* We stop the process here *)
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
+ (* We stop the process here *)
exit 0
end
@@ -364,10 +435,14 @@ let anonymous filename =
raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
let _ =
+ Global.initialize ();
Corelang.add_internal_funs ();
try
Printexc.record_backtrace true;
- Arg.parse Options.options anonymous usage
+
+ let options = Options.options @ (Plugins.options ()) in
+
+ Arg.parse options anonymous usage
with
| Parse.Syntax_err _ | Lexer_lustre.Error _
| Types.Error (_,_) | Clocks.Error (_,_)
@@ -379,428 +454,3 @@ let _ =
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
-=======
-(********************************************************************)
-(* *)
-(* The LustreC compiler toolset / The LustreC Development Team *)
-(* Copyright 2012 - -- ONERA - CNRS - INPT *)
-(* *)
-(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
-(* under the terms of the GNU Lesser General Public License *)
-(* version 2.1. *)
-(* *)
-(********************************************************************)
-
-open Format
-open Log
-
-open Utils
-open LustreSpec
-open Compiler_common
-
-exception StopPhase1 of program
-
-let usage = "Usage: lustrec [options] \x1b[4msource-file\x1b[0m"
-
-let extensions = [".ec"; ".lus"; ".lusi"]
-
-(* print a .lusi header file from a source prog *)
-let print_lusi prog dirname basename extension =
- let header = Lusic.extract_header dirname basename prog in
- let header_name = dirname ^ "/" ^ basename ^ extension in
- let h_out = open_out header_name in
- let h_fmt = formatter_of_out_channel h_out in
- begin
- Typing.uneval_prog_generics header;
- Clock_calculus.uneval_prog_generics header;
- Printers.pp_lusi_header h_fmt basename header;
- close_out h_out
- end
-
-(* compile a .lusi header file *)
-let compile_header dirname basename extension =
- let destname = !Options.dest_dir ^ "/" ^ basename in
- let header_name = basename ^ extension in
- let lusic_ext = extension ^ "c" in
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
- let header = parse_header true (dirname ^ "/" ^ header_name) in
- ignore (Modules.load_header ISet.empty header);
- ignore (check_top_decls header);
- create_dest_dir ();
- Log.report ~level:1
- (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension));
- Lusic.write_lusic true header destname lusic_ext;
- Lusic.print_lusic_to_h destname lusic_ext;
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.")
- end
-
-(* check whether a source file has a compiled header,
- if not, generate the compiled header *)
-let compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension =
- let destname = !Options.dest_dir ^ "/" ^ basename in
- let lusic_ext = extension ^ "c" in
- let header_name = destname ^ lusic_ext in
- begin
- if not (Sys.file_exists header_name) then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
- Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
- Lusic.print_lusic_to_h destname lusic_ext
- end
- else
- let lusic = Lusic.read_lusic destname lusic_ext in
- if not lusic.Lusic.from_lusi then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
- Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
-(*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
- Lusic.print_lusic_to_h destname lusic_ext
- end
- else
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
- Modules.check_dependency lusic destname;
- let header = lusic.Lusic.contents in
- let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in
- check_compatibility
- (prog, computed_types_env, computed_clocks_env)
- (header, declared_types_env, declared_clocks_env)
- end
- end
-
-(* From prog to prog *)
-let stage1 prog dirname basename =
- (* Removing automata *)
- let prog = Automata.expand_decls prog in
-
- (* Importing source *)
- let _ = Modules.load_program ISet.empty prog in
-
- (* Extracting dependencies *)
- let dependencies, type_env, clock_env = import_dependencies prog in
-
- (* Sorting nodes *)
- let prog = SortProg.sort prog in
-
- (* Perform inlining before any analysis *)
- let orig, prog =
- if !Options.global_inline && !Options.main_node <> "" then
- (if !Options.witnesses then prog else []),
- Inliner.global_inline basename prog type_env clock_env
- else (* if !Option.has_local_inline *)
- [],
- Inliner.local_inline basename prog type_env clock_env
- in
-
- (* Checking stateless/stateful status *)
- if Plugins.check_force_stateful () then
- force_stateful_decls prog
- else
- check_stateless_decls prog;
-
- (* Typing *)
- let computed_types_env = type_decls type_env prog in
-
- (* Clock calculus *)
- let computed_clocks_env = clock_decls clock_env prog in
-
- (* Generating a .lusi header file only *)
- if !Options.lusi then
- (* We stop here the processing and produce the current prog. It will be
- exported as a lusi *)
- raise (StopPhase1 prog);
-
- (* Delay calculus *)
- (* TO BE DONE LATER (Xavier)
- if(!Options.delay_calculus)
- then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
- try
- Delay_calculus.delay_prog Basic_library.delay_env prog
- with (Delay.Error (loc,err)) as exc ->
- Location.print loc;
- eprintf "%a" Delay.pp_error err;
- Utils.track_exception ();
- raise exc
- end;
- *)
-
- (* Creating destination directory if needed *)
- create_dest_dir ();
-
- (* Compatibility with Lusi *)
- (* Checking the existence of a lusi (Lustre Interface file) *)
- let extension = ".lusi" in
- compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
-
- Typing.uneval_prog_generics prog;
- Clock_calculus.uneval_prog_generics prog;
-
- if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
- begin
- let orig = Corelang.copy_prog orig in
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
- check_stateless_decls orig;
- let _ = Typing.type_prog type_env orig in
- let _ = Clock_calculus.clock_prog clock_env orig in
- Typing.uneval_prog_generics orig;
- Clock_calculus.uneval_prog_generics orig;
- Inliner.witness
- basename
- !Options.main_node
- orig prog type_env clock_env
- end;
-
- (* Computes and stores generic calls for each node,
- only useful for ANSI C90 compliant generic node compilation *)
- if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
- (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with
- Corelang.Node nd -> Format.eprintf "%s calls %a" id
- Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
-
- (* Optimization of prog:
- - Unfold consts
- - eliminate trivial expressions
- *)
- let prog =
- if !Options.const_unfold || !Options.optimization >= 4 then
- Optimize_prog.prog_unfold_consts prog
- else
- prog
- in
-
- (* Normalization phase *)
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
- (* Special treatment of arrows in lustre backend. We want to keep them *)
- if !Options.output = "lustre" then
- Normalization.unfold_arrow_active := false;
- let prog = Normalization.normalize_prog prog in
- Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
-
- let prog =
- if !Options.mpfr
- then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
- Mpfr.inject_prog prog
- end
- else
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping FP numbers@,");
- prog
- end in
- Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
-
- (* Checking array accesses *)
- if !Options.check then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. array access checks@,");
- Access.check_prog prog;
- end;
-
- prog, dependencies
-
-(* prog -> machine *)
-
-let stage2 prog =
-
- (* Computation of node equation scheduling. It also breaks dependency cycles
- and warns about unused input or memory variables *)
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. scheduling@,");
- let prog, node_schs = Scheduling.schedule_prog prog in
- Log.report ~level:1 (fun fmt -> fprintf fmt "%a" Scheduling.pp_warning_unused node_schs);
- Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
- Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
- Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
- Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
-
-
- (* TODO Salsa optimize prog:
- - emits warning for programs with pre inside expressions
- - make sure each node arguments and memory is bounded by a local annotation
- - introduce fresh local variables for each real pure subexpression
- *)
- (* let prog = *)
- (* if true then *)
- (* Salsa.Prog.normalize prog *)
- (* else *)
- (* prog *)
- (* in *)
-
- (* DFS with modular code generation *)
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@ ");
- let machine_code = Machine_code.translate_prog prog node_schs in
-
- (* Optimize machine code *)
- let machine_code, removed_table =
- if !Options.optimization >= 2 && !Options.output <> "horn" then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@ ");
- Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code
- end
- else
- machine_code, IMap.empty
- in
- (* Optimize machine code *)
- let machine_code =
- if !Options.optimization >= 3 && !Options.output <> "horn" then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@ ");
- let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in
- let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
- Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables)
- end
- else
- machine_code
- in
-
- (* Salsa optimize machine code *)
- Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
- (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
- machine_code);
-
- machine_code
-
-
-let stage3 prog machine_code dependencies basename =
- (* Printing code *)
- let basename = Filename.basename basename in
- let destname = !Options.dest_dir ^ "/" ^ basename in
- match !Options.output with
- "C" ->
- begin
- let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
- let source_lib_file = destname ^ ".c" in (* Could be changed *)
- let source_main_file = destname ^ "_main.c" in (* Could be changed *)
- let makefile_file = destname ^ ".makefile" in (* Could be changed *)
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
- C_backend.translate_to_c
- alloc_header_file source_lib_file source_main_file makefile_file
- basename prog machine_code dependencies
- end
- | "java" ->
- begin
- failwith "Sorry, but not yet supported !"
- (*let source_file = basename ^ ".java" in
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
- let source_out = open_out source_file in
- let source_fmt = formatter_of_out_channel source_out in
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
- Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
- end
- | "horn" ->
- begin
- let source_file = destname ^ ".smt2" in (* Could be changed *)
- let source_out = open_out source_file in
- let fmt = formatter_of_out_channel source_out in
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
- Horn_backend.translate fmt basename prog machine_code;
- (* Tracability file if option is activated *)
- if !Options.horntraces then (
- let traces_file = destname ^ ".traces" in (* Could be changed *)
- let traces_out = open_out traces_file in
- let fmt = formatter_of_out_channel traces_out in
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
- Horn_backend.traces_file fmt basename prog machine_code;
- )
- end
- | "lustre" ->
- begin
- let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
- let source_out = open_out source_file in
- let fmt = formatter_of_out_channel source_out in
- Printers.pp_prog fmt prog;
-(* Lustre_backend.translate fmt basename normalized_prog machine_code *)
- ()
- end
-
- | _ -> assert false
-
-(* compile a .lus source file *)
-let compile_source dirname basename extension =
-
- Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
-
- (* Parsing source *)
- let prog = parse_source (dirname ^ "/" ^ basename ^ extension) in
-
- let prog =
- if !Options.mpfr then
- Mpfr.mpfr_module::prog
- else
- prog
- in
- let prog, dependencies =
- try
- stage1 prog dirname basename
- with StopPhase1 prog -> (
- if !Options.lusi then
- begin
- let lusi_ext = ".lusi" (* extension ^ "i" *) in
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@," (dirname ^ "/" ^ basename ^ lusi_ext));
- print_lusi prog dirname basename lusi_ext;
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
- exit 0
- end
- else
- assert false
- )
- in
-
- let machine_code =
- stage2 prog
- in
-
- let machine_code = Plugins.refine_machine_code prog machine_code in
-
- stage3 prog machine_code dependencies basename;
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
- (* We stop the process here *)
- exit 0
- end
-
-let compile dirname basename extension =
- match extension with
- | ".lusi" -> compile_header dirname basename extension
- | ".lus" -> compile_source dirname basename extension
- | _ -> assert false
-
-let anonymous filename =
- let ok_ext, ext = List.fold_left
- (fun (ok, ext) ext' ->
- if not ok && Filename.check_suffix filename ext' then
- true, ext'
- else
- ok, ext)
- (false, "") extensions in
- if ok_ext then
- let dirname = Filename.dirname filename in
- let basename = Filename.chop_suffix (Filename.basename filename) ext in
- compile dirname basename ext
- else
- raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
-
-let _ =
- Global.initialize ();
- Corelang.add_internal_funs ();
- try
- Printexc.record_backtrace true;
-
- let options = Options.options @ (Plugins.options ()) in
-
- Arg.parse options anonymous usage
- with
- | Parse.Syntax_err _ | Lexer_lustre.Error _
- | Types.Error (_,_) | Clocks.Error (_,_)
- | Corelang.Error _ (*| Task_set.Error _*)
- | Causality.Cycle _ -> exit 1
- | Sys_error msg -> (eprintf "Failure: %s@." msg)
- | exc -> (Utils.track_exception (); raise exc)
-
-(* Local Variables: *)
-(* compile-command:"make -C .." *)
-(* End: *)
->>>>>>> salsa
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index ae9c55fe5ee87f31f86a933e944a3a577f6bd472..afe7d9ae0bc187cb678cf367f94548c1eeed8744 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -45,12 +45,11 @@ let rec eliminate elim instr =
and eliminate_expr elim expr =
match expr.value_desc with
| LocalVar v -> (try IMap.find v.var_id elim with Not_found -> expr)
-<<<<<<< HEAD
- | Fun (id, vl) -> Fun (id, List.map (eliminate_expr elim) vl)
- | Array(vl) -> Array(List.map (eliminate_expr elim) vl)
- | Access(v1, v2) -> Access(eliminate_expr elim v1, eliminate_expr elim v2)
- | Power(v1, v2) -> Power(eliminate_expr elim v1, eliminate_expr elim v2)
- | Cst _ -> expr
+ | Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)}
+ | Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
+ | Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
+ | Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
+ | Cst _ | StateVar _ -> expr
let eliminate_dim elim dim =
Dimension.expr_replace_expr
@@ -59,11 +58,16 @@ let eliminate_dim elim dim =
with Not_found -> mkdim_ident dim.dim_loc v)
dim
+
+(* 8th Jan 2016: issues when merging salsa with horn_encoding: The following
+ functions seem unsused. They have to be adapted to the new type for expr
+
+
let unfold_expr_offset m offset expr =
List.fold_left
(fun res ->
(function Index i ->
- Access(res, value_of_dimension m i)
+ Access(res, value_of_dimension m i)
| Field f -> failwith "not yet implemented"))
expr offset
@@ -80,7 +84,7 @@ let rec simplify_cst_expr m offset cst =
| _ -> (Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@." Printers.pp_const cst; assert false)
let simplify_expr_offset m expr =
- let rec simplify offset expr =
+ let rec simplify offset expr_desc =
match offset, expr with
| Field f ::q , _ -> failwith "not yet implemented"
| _ , Fun (id, vl) when Basic_library.is_internal_fun id
@@ -98,7 +102,7 @@ let simplify_expr_offset m expr =
(* | _ -> (Format.eprintf "internal error: Optimize_machine.simplify_expr_offset %a@." pp_val expr; assert false) *)
(*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)
with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)
- in simplify [] expr
+ in { expr with value_desc = simplify [] expr_desc }
let rec simplify_instr_offset m accu instr =
match instr with
@@ -119,13 +123,7 @@ let rec simplify_instr_offset m accu instr =
and simplify_instrs_offset m instrs =
let rev_l = List.fold_left (simplify_instr_offset m) [] instrs in
List.rev rev_l
-=======
- | Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)}
- | Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
- | Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
- | Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
- | Cst _ | StateVar _ -> expr
->>>>>>> salsa
+*)
let is_scalar_const c =
match c with