### Profile

Statistics
| Branch: | Tag: | Revision:

## lustrec / src / checks / algebraicLoop.ml @ 04a188ec

 1 ```(* We try to solve all algebraic loops (AL) from prog: ``` ```each node is mapped to its own cycles ``` ```each cycle is tentatively solved by inlining one of its component ``` ```When done, a report is generated. ``` ```- for each initial AL, the cycle is presented ``` ``` - either it is solvable and we provide the set of inlines that solves it ``` ``` - or it is not and we write the AL as unsolvable by inlining ``` ``` If the option solve_al is activated, the resulting partially inlined prog is ``` ``` propagated fur future processing Otherwise the compilation stops ``` ```*) ``` ```open Lustre_types ``` ```open Corelang ``` ```open Utils ``` ```(* An single algebraic loop is defined (partition, node calls, inlined, status) ``` ``` ie ``` ``` 1. the list of variables in the loop, ident list ``` ``` ``` ``` 2.the possible functions identifier to inline, and whether they have been ``` ``` inlined yet (ident * tag * bool) list and ``` ``` 3. a status whether the inlining is enough bool ``` ```*) ``` ```type call = ident * expr * eq (* fun id, expression, and containing equation *) ``` ``` ``` ```type algebraic_loop = ident list * (call * bool) list * bool ``` ```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. *) ``` ```module CycleResolution = ``` ```struct ``` ``` (* We iter over calls in node defs. If the call defined on of the variable in ``` ``` the cycle, we store it for future possible inline. *) ``` ``` let resolve node partition : call list = ``` ``` let partition = ISet.of_list partition in ``` ``` (* Preprocessing calls: associate to each of them the eq.lhs associated *) ``` ``` let calls_expr = Causality.NodeDep.get_calls (fun _ -> true) node in ``` ``` let eqs, auts = get_node_eqs node in ``` ``` assert (auts = []); (* TODO voir si on peut acceder directement aux eqs qui font les calls *) ``` ``` let calls = List.map ( ``` ``` fun expr -> ``` ``` let eq = List.find (fun eq -> ``` ``` Corelang.expr_contains_expr expr.expr_tag eq.eq_rhs ``` ``` ) eqs in ``` ``` let fun_name = match expr.expr_desc with ``` ``` | Expr_appl(fun_id, _, _) -> fun_id ``` ``` | _ -> assert false ``` ``` in ``` ``` fun_name, expr, eq ``` ``` ) calls_expr in ``` ``` List.fold_left ( ``` ``` fun accu ((_, _, eq) as call) -> ``` ``` let shared_vars = ISet.inter (ISet.of_list eq.eq_lhs) partition in ``` ``` if not (ISet.is_empty shared_vars) then ``` ``` (* We have a match: keep the eq and the expr to inline *) ``` ``` call::accu ``` ``` else ``` ``` accu ``` ``` ) [] calls ``` ```end ``` ```(* Format.fprintf fmt "@[Possible resolution:@ %a@]" pp_resolution resolution*) ``` ``` ``` ```let pp_resolution fmt resolution = ``` ``` fprintf_list ~sep:"@ " (fun fmt (eq, tag) -> ``` ``` Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq ``` ``` ) fmt resolution ``` ``` ``` ```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 *) ``` ```(* expression *) ``` ```(**********************************************************************) ``` ```let inline_annotation loc = ``` ``` Inliner.keyword, ``` ``` Corelang.mkeexpr loc ``` ``` (Corelang.mkexpr loc ``` ``` (Expr_const (Const_tag tag_true) )) ``` ```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 -> ( ``` ``` (* 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 "@[%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 node expr = ``` ``` (* Format.eprintf "inlining %a@ @?" Printers.pp_expr expr; *) ``` ``` let ann = inline_annotation expr.expr_loc in ``` ``` 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 "@[Fast revalidation: normalization + schedulability@ "); ``` ``` Options.verbose_level := !Options.verbose_level - 2; ``` ``` (* Mini stage 1 *) ``` ``` (* Extracting dependencies: fill some table with typing info *) ``` ``` (* ignore (Modules.load ~is_header:false prog); REMOVED on 2019/07/16 *) ``` ``` (* 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 ``` ``` Compiler_common.check_stateless_decls prog; ``` ``` (* Typing *) ``` ``` let _ (*computed_types_env*) = Compiler_common.type_decls !Global.type_env prog in ``` ``` (* Clock calculus *) ``` ``` let _ (*computed_clocks_env*) = Compiler_common.clock_decls !Global.clock_env prog in ``` ``` (* Normalization *) ``` ``` let params = Backends.get_normalization_params () in ``` ``` let prog = Normalization.normalize_prog params 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 max_inlines prog nd existing_al partitions = ``` ``` (* let pp_calls = pp_calls nd in *) ``` ``` (* For each partition, we identify the original one *) ``` ``` 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 ``` ``` (* Identifying previous alarms that could be associated to current conflict *) ``` ``` let matched, non_matched = List.partition match_al existing_al in ``` ``` 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: @[inlined: {%a}@ no inlined: {%a}@ @]@ " *) ``` ``` (* pp_calls previous_inlined *) ``` ``` (* pp_calls previous_no_inlined *) ``` ``` (* ; *) ``` ``` ``` ``` 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 && 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 ``` ``` In case of failure, ie. inlining does not solve the problem; the status is false. ``` ``` 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 : program_t * bool * report = ``` ``` let max_inlines = !Options.al_nb_max in ``` ```(* We iterate over each node *) ``` ``` let _, prog, al_list = ``` ``` List.fold_right ( ``` ``` fun top (max_inlines, prog_accu, al_list) -> ``` ``` match top.top_decl_desc with ``` ``` | Node nd -> ( ``` ``` let error, max_inlines = ``` ``` try (* without exception the node is schedulable; nothing to declare *) ``` ``` let _ = Scheduling.schedule_node nd in ``` ``` None, max_inlines ``` ``` with Causality.Error (Causality.DataCycle partitions) -> ( ``` ``` Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@[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 -> 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 *) ``` ``` max_inlines, ``` ``` {top with top_decl_desc = Node nd}::prog_accu, ``` ``` (nd, al)::al_list ``` ``` ) ``` ``` | _ -> 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 nd fmt (partition, calls, status) = ``` ``` let open Format in ``` ``` fprintf fmt "@["; ``` ``` fprintf fmt "variables in the alg. loop: @[%a@]@ " ``` ``` (fprintf_list ~sep:",@ " pp_print_string) partition; ``` ``` fprintf fmt "@ involved node calls: @[%a@]@ " ``` ``` (fprintf_list ~sep:",@ " ``` ``` (fun fmt ((funid, expr, eq), status) -> ``` ``` fprintf fmt "%s" funid; ``` ``` if status && is_expr_inlined nd expr then fprintf fmt " (inlining it solves the alg. loop)"; ``` ``` ) ``` ``` ) calls; ``` ``` fprintf fmt "@]" ``` ``` (* TODO ploc: ``` ``` First analyse the cycle and identify a list of nodes to be inlined, or node instances ``` ``` Then two behaviors: ``` ``` - print that list instead of the unreadable cyclic dependency comment ``` ``` - modify the node by adding the inline information ``` ``` - recall the subset of stage1 but restricted to a single node: ``` ``` - inline locally, typing, clocking (may have to reset the tables first), normalization of the node, mpfr injection ``` ``` - recall stage2 ``` ``` *) ``` ``` ``` ``` ``` ```let pp_report fmt report = ``` ``` let open Format in ``` ``` fprintf_list ~sep:"@." ``` ``` (fun fmt (nd, als) -> ``` ``` let top = Corelang.node_from_name (nd.node_id) in ``` ``` 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 "algebraic loop in node %s: {@[%a@]}" ``` ``` nd.node_id ``` ``` (fprintf_list ~sep:"@ " (pp_al nd)) als ``` ``` ) ``` ``` ) fmt report; ``` ``` fprintf fmt "@." ``` ``` ``` ```let analyze cpt prog = ``` ``` Log.report ~level:1 (fun fmt -> ``` ``` Format.fprintf fmt "@[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 ``` ``` ``` ``` 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 (Error.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 ``` ``` ``` ``` ```