From 264a4844995eb33f236f8b642b79138883cc96d2 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Thu, 20 Jul 2017 13:20:04 -0700
Subject: [PATCH] First working version of algebraic loop resolution. Disabled
by default.
---
.gitignore | 6 +-
src/algebraicLoop.ml | 354 +++++++++++++++++++++++-------------
src/corelang.ml | 3 +-
src/error.ml | 5 +-
src/inliner.ml | 67 +++++--
src/machine_code.ml | 2 +-
src/main_lustre_compiler.ml | 6 +-
src/main_lustre_testgen.ml | 2 +-
src/options.ml | 3 +-
src/options_management.ml | 2 +
10 files changed, 292 insertions(+), 158 deletions(-)
diff --git a/.gitignore b/.gitignore
index c1292d11..5acf3044 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,6 @@
-/_build/
-/main_lustre_compiler.native
+*~
+/src/_build/
/setup.data
/setup.log
/src/version.ml
-/myocamlbuild.ml
\ No newline at end of file
+/myocamlbuild.ml
diff --git a/src/algebraicLoop.ml b/src/algebraicLoop.ml
index 53633eeb..f863bb7e 100644
--- a/src/algebraicLoop.ml
+++ b/src/algebraicLoop.ml
@@ -14,7 +14,6 @@ When done, a report is generated.
open LustreSpec
open Corelang
open Utils
-open Format
(* An single algebraic loop is defined (partition, node calls, inlined, status)
ie
@@ -30,8 +29,9 @@ open Format
type call = ident * expr * eq (* fun id, expression, and containing equation *)
type algebraic_loop = ident list * (call * bool) list * bool
-
-exception Error of (node_desc * (algebraic_loop list)) list
+type report = (node_desc * algebraic_loop list) list
+exception Error of report
+
(* Module that extract from the DataCycle the set of node that could be inlined
to solve the problem. *)
@@ -76,7 +76,7 @@ let pp_resolution fmt resolution =
Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq
) fmt resolution
-let al_is_solved (_, (vars, calls, status)) = status
+let al_is_solved (_, als) = List.for_all (fun (vars, calls, status) -> status) als
(**********************************************************************)
(* Functions to access or toggle the local inlining feature of a call *)
@@ -89,124 +89,181 @@ let inline_annotation loc =
(Corelang.mkexpr loc
(Expr_const (Const_tag tag_true) ))
-let is_expr_inlined expr =
+let is_inlining_annot (key, status) =
+key = Inliner.keyword && (
+ match status.eexpr_qfexpr.expr_desc with
+ | Expr_const (Const_tag tag) when tag = tag_true ->
+ true
+ | Expr_const (Const_tag tag) when tag = tag_false ->
+ false
+ | _ -> assert false (* expecting true or false value *)
+)
+
+let is_expr_inlined nd expr =
match expr.expr_annot with
None -> false
- | Some anns -> if List.mem_assoc Inliner.keyword anns.annots then
- let status = List.assoc Inliner.keyword anns.annots in
- match status.eexpr_qfexpr.expr_desc with
- | Expr_const (Const_tag tag) when tag = tag_true ->
- true
- | Expr_const (Const_tag tag) when tag = tag_false ->
- false
- | _ -> assert false (* expecting true or false value *)
- else false
-
+ | Some anns -> (
+ (* Sanity check: expr should have the annotation AND the annotation should be declared *)
+ let local_ann = List.exists is_inlining_annot anns.annots in
+ let all_expr_inlined = Hashtbl.find_all Annotations.expr_annotations Inliner.keyword in
+ let registered =
+ List.exists
+ (fun (nd_id, expr_tag) -> nd_id = nd.node_id && expr_tag = expr.expr_tag)
+ all_expr_inlined
+ in
+ match local_ann, registered with
+ | true, true -> true (* Everythin' all righ' ! *)
+ | false, false -> false (* idem *)
+ | _ -> assert false
+ )
+
+let pp_calls nd fmt calls = Format.fprintf fmt "@[<v 0>%a@]"
+ (fprintf_list ~sep:"@ " (fun fmt (funid,expr, _) -> Format.fprintf fmt "%s: %i (inlined:%b)"
+ funid
+ expr.expr_tag
+ (is_expr_inlined nd expr)
+ ))
+ calls
+
(* Inline the provided expression *)
-let inline_expr expr =
+let inline_expr node expr =
+ (* Format.eprintf "inlining %a@ @?" Printers.pp_expr expr; *)
let ann = inline_annotation expr.expr_loc in
- match expr.expr_annot with
- | None -> expr.expr_annot = Some {annots = [ann]; annot_loc = expr.expr_loc}
- | Some anns -> expr.expr_annot = Some {anns with annots = ann::anns.annots}
-
-(* Inline the call tagged tag in expr: should not be used anymore, thanks to a direct call to inline_expr *)
-let rec inline_call tag expr =
- if expr.expr_tag = tag then
- inline_expr expr
+ let ann = {annots = [ann]; annot_loc = expr.expr_loc} in
+ let res = update_expr_annot node.node_id expr ann in
+ (* assert (is_expr_inlined node res); *)
+ (* Format.eprintf "Is expression inlined? %b@." (is_expr_inlined node res); *)
+ res
+
+(* Perform the steps of stage1/stage2 to revalidate the schedulability of the program *)
+let fast_stages_processing prog =
+ Log.report ~level:3
+ (fun fmt -> Format.fprintf fmt "@[<v 2>Fast revalidation: normalization + schedulability@ ");
+ Options.verbose_level := !Options.verbose_level - 2;
+
+ (* Mini stage 1 *)
+ (* Extracting dependencies *)
+ let dependencies, type_env, clock_env = Compiler_common.import_dependencies prog in
+ (* Local inlining *)
+ let prog = Inliner.local_inline prog (* type_env clock_env *) in
+ (* Checking stateless/stateful status *)
+ if Plugins.check_force_stateful () then
+ Compiler_common.force_stateful_decls prog
else
- let _in = inline_call tag in
- let _ins = List.exists _in
- in
- match expr.expr_desc with
- | Expr_const _
- | Expr_ident _ -> false
- | Expr_tuple el -> _ins el
- | Expr_ite (g,t,e) -> _ins [g;t;e]
- | Expr_arrow (e1, e2)
- | Expr_fby (e1, e2) -> _ins [e1; e2]
- | Expr_array el -> _ins el
- | Expr_access (e, _)
- | Expr_power (e, _)
- | Expr_pre e
- | Expr_when (e, _, _) -> _in e
- | Expr_merge (_, hl) -> _ins (List.map snd hl)
- | Expr_appl (_, arg, Some r) -> _ins [arg; r]
- | Expr_appl (_, arg, None) -> _in arg
+ Compiler_common.check_stateless_decls prog;
+ (* Typing *)
+ let _ (*computed_types_env*) = Compiler_common.type_decls type_env prog in
+ (* Clock calculus *)
+ let _ (*computed_clocks_env*) = Compiler_common.clock_decls clock_env prog in
+ (* Normalization *)
+ let prog = Normalization.normalize_prog ~backend:!Options.output prog in
+ (* Mini stage 2 : Scheduling *)
+ let res = Scheduling.schedule_prog prog in
+ Options.verbose_level := !Options.verbose_level + 2;
+ Log.report ~level:3
+ (fun fmt -> Format.fprintf fmt "@]@ ");
+ res
(**********************)
(* Returns a modified node, if possible, and an algebraic_loop report *)
-let rec solving_node nd existing_al partitions =
+let rec solving_node max_inlines prog nd existing_al partitions =
+ (* let pp_calls = pp_calls nd in *)
(* For each partition, we identify the original one *)
- let rerun, al = List.fold_left (fun (rerun, al) part ->
+ let rerun, max_inlines, al = List.fold_left (fun (rerun, inlines, al) part ->
let part_vars = ISet.of_list part in
+ (* Useful functions to filter list of elements *)
let match_al (vars, calls, status) =
- not (ISet.is_empty (ISet.inter (ISet.of_list vars) part_vars)) in
+ not (ISet.is_empty (ISet.inter (ISet.of_list vars) part_vars)) in
+ (* Identifying previous alarms that could be associated to current conflict *)
let matched, non_matched = List.partition match_al existing_al in
- match matched, non_matched with
- | [], _ -> ((* A new conflict partition *)
- let calls = CycleResolution.resolve nd part in
- (* Filter out already inlined calls *)
- let already_inlined, possible_resolution =
- List.partition (fun (_, expr, _) -> is_expr_inlined expr) calls in
- (* Inlining the first uninlined call *)
- match possible_resolution with
- | (eq, expr, fun_id)::_ -> ((* One could inline expr *)
- (* Forcing the expr to be inlined *)
- let _ = inline_expr expr in
- true, (* we have to rerun to see if the inlined expression solves the issue *)
- (
- part,
- List.map (fun (eq, expr2, fcn_name) -> fcn_name, expr2, (expr2.expr_tag = expr.expr_tag)) calls,
- false (* Status is nok, LA is unsolved yet *)
-
- )::non_matched
- )
- | [] -> (* No more calls to inline: algebraic loop is not solvable *)
- rerun, (* we don't force rerun since the current node is not solvable *)
- (
- part, (* initial list of troublesome variables *)
- List.map (fun (eq, expr, fcn_name) -> fcn_name, expr, false) calls,
- false (* Status is nok, LA is unsolved *)
- )::non_matched
-
- )
- | [vars, calls, status], _ ->
- assert false (* Existing partitions were already addressed:
- on peut regarder si la partition courante concerne xxx
- else (* New cycle ??? *)
-
-
-
-
- Que faut il faire?
-
- dans un premiertemps on peut ramasser les contraintes et s'arreter là .
- pas d'appel recursif donc on a toujours des nouvelles partitions
- on calcule les apples, on les associe à faux (on a pas inliné encore)
- et le statue global est à faux (on a rien resolu)
-
- comment resoud-on ?
- on ne doit se focaliser que sur les partitions courantes. C'est elle qui sont en conflit
- pour chaque, on pick un call et on l'inlinee
- apres on appel stage1/stage2 pour faire le scheudling du node
-
-
- *)
+ let previous_calls =
+ match matched with
+ | [] -> []
+ | [_ (*vars*), calls, _ (*status*)] -> List.map fst calls (* we just keep the calls *)
+ | _ -> (* variable should not belong to two different algrebraic loops. At least I
+ hope so! *)
+ assert false
+ in
+ let match_previous (eq, expr, fun_id) =
+ List.exists
+ (fun (_, expr', _) -> expr'.expr_tag = expr.expr_tag)
+ previous_calls
+ in
+ (* let match_inlined (_, expr, _) = is_expr_inlined nd expr in *)
+
+ (* let previous_inlined, previous_no_inlined = List.partition match_inlined previous_calls in *)
+ (* Format.eprintf "Previous calls: @[<v 0>inlined: {%a}@ no inlined: {%a}@ @]@ " *)
+ (* pp_calls previous_inlined *)
+ (* pp_calls previous_no_inlined *)
-
- ) (false, existing_al) partitions
+ (* ; *)
+
+ let current_calls = CycleResolution.resolve nd part in
+ (* Format.eprintf "Current calls: %a" pp_calls current_calls; *)
+ (* Filter out calls from current_calls that were not already in previous calls *)
+ let current_calls = List.filter (fun c -> not (match_previous c)) current_calls
+ in
+ (* Format.eprintf "Current new calls (no old ones): %a" pp_calls current_calls; *)
+ let calls = previous_calls @ current_calls in
+ (* Format.eprintf "All calls (previous + new): %a" pp_calls calls; *)
+
+ (* Filter out already inlined calls: actually they should not appear
+ ... since they were inlined. We keep it for safety. *)
+ let _ (* already_inlined *), possible_resolution =
+ List.partition (fun (_, expr, _) -> is_expr_inlined nd expr) calls in
+ (* Inlining the first uninlined call *)
+ match possible_resolution with
+ | (fun_id, expr, eq)::_ -> ((* One could inline expr *)
+ Log.report ~level:2 (fun fmt-> Format.fprintf fmt "inlining call to %s@ " fun_id);
+ (* Forcing the expr to be inlined *)
+ let _ = inline_expr nd expr in
+ (* Format.eprintf "Making sure that the inline list evolved: inlined = {%a}" *)
+ (* pp_calls *)
+ (* ; *)
+ true, (* we have to rerun to see if the inlined expression solves the issue *)
+ max_inlines - 1,
+ (
+ part,
+ List.map (fun ((eq, expr2, fcn_name) as call)-> call, (expr2.expr_tag = expr.expr_tag)) calls,
+ true (* TODO was false. Should be put it true and expect a final
+ scheduling to change it to false in case of failure ? *) (*
+ Status is nok, LA is unsolved yet *)
+
+ )::non_matched
+ )
+ | [] -> (* No more calls to inline: algebraic loop is not solvable *)
+ rerun, (* we don't force rerun since the current node is not solvable *)
+ max_inlines,
+ (
+ part, (* initial list of troublesogme variables *)
+ List.map (fun ((eq, expr, fcn_name) as call) -> call, false) calls,
+ false (* Status is nok, LA is unsolved *)
+ )::non_matched
+
+ ) (false, max_inlines, existing_al) partitions
in
(* if partition an already identified al ? *)
(* if ISet.of_list partition *)
-
- (* if rerun then *)
- (* assert false (\* the missing part, redo stage 1, ... with the updated inline flags *\) *)
- (* ; *)
- (* TODO xxx il faut ici ajouter le inline sur le 1er appel,
- puis reafaire le stage1 et scheduling du noeud *)
- Some(nd, al)
-
+ if rerun && max_inlines > 0 then
+ (* At least one partition could be improved: we try to inline the calls and reschedule the node. *)
+ try
+ Log.report ~level:2 (fun fmt -> Format.fprintf fmt "rescheduling node with new inlined call@ ");
+ let _ = fast_stages_processing prog in
+ (* If everything went up to here, the problem is solved! All associated
+ alarms are mapped to valid status. *)
+ let al = List.map (fun (v,c,_) -> v,c,true) al in
+ Log.report ~level:2 (fun fmt -> Format.fprintf fmt "AL solved@ ");
+ Some(nd, al), max_inlines
+ with Causality.Error (Causality.DataCycle partitions2) -> (
+ Log.report ~level:3 (fun fmt -> Format.fprintf fmt "AL not solved yet. Further processing.@ ");
+ solving_node max_inlines prog nd al partitions2
+ )
+ else ((* No rerun, we return the current node and computed alarms *)
+ Log.report ~level:3 (fun fmt -> Format.fprintf fmt "AL not solved yet. Stopping.@ ");
+ Some(nd, al), max_inlines
+ )
+
(** This function takes a prog and returns (prog', status, alarms)
where prog' is a modified prog with some locally inlined calls
status is true is the final prog' is schedulable, ie no algebraic loop
@@ -214,42 +271,51 @@ let rec solving_node nd existing_al partitions =
Alarms contain the list of inlining performed or advised for each node.
This could be provided as a feedback to the user.
*)
-let clean_al prog =
+let clean_al prog : program * bool * report =
+ let max_inlines = !Options.al_nb_max in
(* We iterate over each node *)
- let prog, al_list =
+ let _, prog, al_list =
List.fold_right (
- fun top (prog_accu, al_list) ->
+ fun top (max_inlines, prog_accu, al_list) ->
match top.top_decl_desc with
| Node nd -> (
- let error =
+ let error, max_inlines =
try (* without exception the node is schedulable; nothing to declare *)
let _ = Scheduling.schedule_node nd in
- None
- with Causality.Error (Causality.DataCycle partitions) -> solving_node nd [] partitions
+ None, max_inlines
+ with Causality.Error (Causality.DataCycle partitions) -> (
+ Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@[<v 2>AL in node %s@ " nd.node_id);
+ let error, max_inlines = solving_node max_inlines prog nd [] partitions in
+ Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@ @]");
+ error, max_inlines
+ )
in
match error with
- | None -> top::prog_accu, al_list (* keep it as is *)
+ | None -> max_inlines, top::prog_accu, al_list (* keep it as is *)
| Some (nd, al) ->
(* returning the updated node, possible solved, as well as the
generated alarms *)
- {top with top_decl_desc = Node nd}::prog_accu, (nd, al)::al_list
+ max_inlines,
+ {top with top_decl_desc = Node nd}::prog_accu,
+ (nd, al)::al_list
)
- | _ -> top::prog_accu, al_list
- ) prog ([], [])
+ | _ -> max_inlines, top::prog_accu, al_list
+ ) prog (max_inlines, [], [])
in
prog, List.for_all al_is_solved al_list, al_list
(* (ident list * (ident * expr* bool) list * bool) *)
-let pp_al fmt (partition, calls, status) =
+let pp_al nd fmt (partition, calls, status) =
+ let open Format in
fprintf fmt "@[<v 0>";
fprintf fmt "variables in the alg. loop: @[<hov 0>%a@]@ "
(fprintf_list ~sep:",@ " pp_print_string) partition;
fprintf fmt "@ involved node calls: @[<v 0>%a@]@ "
(fprintf_list ~sep:",@ "
- (fun fmt (funid, expr, status) ->
+ (fun fmt ((funid, expr, eq), status) ->
fprintf fmt "%s" funid;
- if status && is_expr_inlined expr then fprintf fmt " (inlining it solves the alg. loop)";
+ if status && is_expr_inlined nd expr then fprintf fmt " (inlining it solves the alg. loop)";
)
) calls;
fprintf fmt "@]"
@@ -265,26 +331,54 @@ let pp_al fmt (partition, calls, status) =
let pp_report fmt report =
- fprintf fmt "@.Algebraic loops in nodes@.";
+ let open Format in
fprintf_list ~sep:"@."
(fun fmt (nd, als) ->
let top = Corelang.node_from_name (nd.node_id) in
- Error.pp_error top.top_decl_loc
+ let pp =
+ if not !Options.solve_al || List.exists (fun (_,_,valid) -> not valid) als then
+ Error.pp_error (* at least one failure: erroneous node *)
+ else
+ Error.pp_warning (* solvable cases: warning only *)
+ in
+ pp top.top_decl_loc
(fun fmt ->
- fprintf fmt "node %s: {@[<v 0>%a@]}"
+ fprintf fmt "algebraic loop in node %s: {@[<v 0>%a@]}"
nd.node_id
- (fprintf_list ~sep:"@ " pp_al) als
+ (fprintf_list ~sep:"@ " (pp_al nd)) als
)
) fmt report;
fprintf fmt "@."
-let analyze prog =
+
+let analyze cpt prog =
+ Log.report ~level:1 (fun fmt ->
+ Format.fprintf fmt "@[<v 2>Algebraic loop detected: ";
+ if !Options.solve_al then Format.fprintf fmt "solving mode actived";
+ Format.fprintf fmt "@ ";
+ );
let prog, status_ok, report = clean_al prog in
- if !Options.solve_al && status_ok then
- Scheduling.schedule_prog prog
- else (
- (* TODO create a report *)
- Format.eprintf "%a" pp_report report;
- raise (Corelang.Error (Location.dummy_loc, Error.AlgebraicLoop))
- )
+
+ let res =
+ if cpt > 0 && !Options.solve_al && status_ok then (
+ try
+ fast_stages_processing prog
+ with _ -> assert false (* Should not happen since the error has been
+ catched already *)
+ )
+ else (
+ (* We stop with unresolved AL *)(* TODO create a report *)
+ (* Printing the report on stderr *)
+ Format.eprintf "%a" pp_report report;
+ raise (Corelang.Error (Location.dummy_loc, Error.AlgebraicLoop))
+ )
+ in
+ (* Printing the report on stderr *)
+ Format.eprintf "%a" pp_report report;
+ res
+
+let analyze prog =
+ analyze !Options.al_nb_max prog
+
+
diff --git a/src/corelang.ml b/src/corelang.ml
index 67c7030a..694ba1b5 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -178,7 +178,8 @@ let update_expr_annot node_id e annot =
List.iter (fun (key, _) ->
Annotations.add_expr_ann node_id e.expr_tag key
) annot.annots;
- { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
+ e.expr_annot <- merge_expr_annot e.expr_annot (Some annot);
+ e
let mkinstr ?lustre_expr ?lustre_eq i =
diff --git a/src/error.ml b/src/error.ml
index 1d4fe3cd..b5a67432 100644
--- a/src/error.ml
+++ b/src/error.ml
@@ -50,10 +50,9 @@ let return_code kind =
"library %s.lusic has a different version number and may crash compiler.@.Please recompile the corresponding interface or source file.@."
sym
-let pp_warning loc warning_code pp_msg =
- Format.eprintf "%a@.Warning %i: %t@."
+let pp_warning loc pp_msg =
+ Format.eprintf "%a@.Warning: %t@."
Location.pp_loc loc
- warning_code
pp_msg
let pp_error loc pp_msg =
diff --git a/src/inliner.ml b/src/inliner.ml
index 05f1394e..0aab3f3d 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -229,7 +229,8 @@ let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
as arguments nodes *)
(not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated,
it is explicitely inlined here *)
- then
+ then (
+ (* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *)
(* The node should be inlined *)
(* let _ = Format.eprintf "Inlining call to %s@." id in *)
let called = try List.find (check_node_name id) nodes
@@ -239,6 +240,7 @@ let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
let expr, locals', eqs'', asserts'', annots'' =
inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
+ )
else
(* let _ = Format.eprintf "Not inlining call to %s@." id in *)
{ expr with expr_desc = Expr_appl(id, args', reset)},
@@ -458,23 +460,58 @@ let global_inline basename prog type_env clock_env =
*)
res
-let local_inline basename prog type_env clock_env =
+let pp_inline_calls fmt prog =
let local_anns = Annotations.get_expr_annotations keyword in
- if local_anns != [] then (
- let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in
- ISet.iter (fun node_id -> Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns;
- List.fold_right (fun top accu ->
- ( match top.top_decl_desc with
- | Node nd when ISet.mem nd.node_id nodes_with_anns ->
- { top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) }
- | _ -> top
- )::accu) prog []
-
-)
- else
+ let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in
+ Format.fprintf fmt "@[<v 0>Inlined expresssions in node (by tags):@ %a@]"
+ (fprintf_list ~sep:""
+ (fun fmt top ->
+ match top.top_decl_desc with
+ | Node nd when ISet.mem nd.node_id nodes_with_anns ->
+ Format.fprintf fmt "%s: {@[<v 0>%a}@]@ "
+ nd.node_id
+ (fprintf_list ~sep:"@ " (fun fmt tag -> Format.fprintf fmt "%i" tag))
+ (List.fold_left
+ (fun accu (id, tag) -> if id = nd.node_id then tag::accu else accu)
+ []
+ local_anns
+ )
+ (* | Node nd -> Format.fprintf fmt "%s: no inline annotations" nd.node_id *)
+ | _ -> ()
+ ))
+ prog
+
+
+let local_inline prog (* type_env clock_env *) =
+ Log.report ~level:2 (fun fmt -> Format.fprintf fmt ".. @[<v 2>Inlining@,");
+ let local_anns = Annotations.get_expr_annotations keyword in
+ let prog =
+ if local_anns != [] then (
+ let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in
+ ISet.iter (fun node_id -> Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Node %s has local expression annotations@ " node_id))
+ nodes_with_anns;
+ List.fold_right (fun top accu ->
+ ( match top.top_decl_desc with
+ | Node nd when ISet.mem nd.node_id nodes_with_anns ->
+ Log.report ~level:2 (fun fmt -> Format.fprintf fmt "[local inline] Processing node %s@ " nd.node_id);
+ let inlined_node = inline_node ~selection_on_annotation:true nd prog in
+ (* Format.eprintf "Before inline@.%a@.After:@.%a@." *)
+ (* Printers.pp_node nd *)
+ (* Printers.pp_node inlined_node; *)
+ { top with top_decl_desc = Node inlined_node }
+
+ | _ -> top
+ )::accu) prog []
+
+ )
+ else (
+ Log.report ~level:2 (fun fmt -> Format.fprintf fmt "No local inline information!@ ");
+ prog
+ )
+ in
+ Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@]@,");
prog
-
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 0e8a5305..eca08aec 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -156,7 +156,7 @@ let rec is_const_value v =
(* Returns the declared stateless status and the computed one. *)
let get_stateless_status m =
- (m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless)
+ (m.mname.node_dec_stateless, try Utils.desome m.mname.node_stateless with _ -> failwith ("stateless status of machine " ^ m.mname.node_id ^ " not computed"))
let is_input m id =
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 3b78406e..ba623572 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -116,7 +116,7 @@ let stage1 prog dirname basename =
Inliner.global_inline basename prog type_env clock_env
else (* if !Option.has_local_inline *)
[],
- Inliner.local_inline basename prog type_env clock_env
+ Inliner.local_inline prog (* type_env clock_env *)
in
(* Checking stateless/stateful status *)
@@ -241,7 +241,7 @@ let stage1 prog dirname basename =
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@,");
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
let prog, node_schs =
try
Scheduling.schedule_prog prog
@@ -254,7 +254,7 @@ let stage2 prog =
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);
-
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
(* TODO Salsa optimize prog:
- emits warning for programs with pre inside expressions
diff --git a/src/main_lustre_testgen.ml b/src/main_lustre_testgen.ml
index 798e5477..4db9362a 100644
--- a/src/main_lustre_testgen.ml
+++ b/src/main_lustre_testgen.ml
@@ -45,7 +45,7 @@ let stage1 prog dirname basename =
Inliner.global_inline basename prog type_env clock_env
else (* if !Option.has_local_inline *)
[],
- Inliner.local_inline basename prog type_env clock_env
+ Inliner.local_inline prog (* type_env clock_env *)
in
check_stateless_decls prog;
diff --git a/src/options.ml b/src/options.ml
index 91a2261f..f70e0b24 100755
--- a/src/options.ml
+++ b/src/options.ml
@@ -53,7 +53,8 @@ let gen_mcdc = ref false
let no_mutation_suffix = ref false
let solve_al = ref false
-
+let al_nb_max = ref 15
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/options_management.ml b/src/options_management.ml
index 33d74b8a..1a052fb4 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -81,6 +81,8 @@ let common_options =
"-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
"-print-types", Arg.Set print_types, "prints node types";
"-print-clocks", Arg.Set print_clocks, "prints node clocks";
+ "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops";
+ "-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops <default: 15>";
"-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
"-version", Arg.Unit print_version, " displays the version";
]
--
GitLab