Profile

1 2 3 ca7ff3f7 Lélio Brun ```(* 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 ``` 9094307a ploc ca7ff3f7 Lélio Brun ``` When done, a report is generated. ``` 9094307a ploc ca7ff3f7 Lélio Brun ``` - 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 ``` 9094307a ploc ``` If the option solve_al is activated, the resulting partially inlined prog is ``` ca7ff3f7 Lélio Brun ``` propagated fur future processing Otherwise the compilation stops *) ``` 8446bf03 ploc ```open Lustre_types ``` 9094307a ploc ```open Corelang ``` ```open Utils ``` ```(* An single algebraic loop is defined (partition, node calls, inlined, status) ``` ca7ff3f7 Lélio Brun ``` ie ``` 23ce017b ploc ``` 1. the list of variables in the loop, ident list ``` ca7ff3f7 Lélio Brun 23ce017b ploc ``` 2.the possible functions identifier to inline, and whether they have been ``` ca7ff3f7 Lélio Brun ``` inlined yet (ident * tag * bool) list and ``` ``` 3. a status whether the inlining is enough bool *) ``` 23ce017b ploc ca7ff3f7 Lélio Brun ```type call = ident * expr * eq ``` ```(* fun id, expression, and containing equation *) ``` 23ce017b ploc ```type algebraic_loop = ident list * (call * bool) list * bool ``` ca7ff3f7 Lélio Brun 264a4844 ploc ```type report = (node_desc * algebraic_loop list) list ``` ca7ff3f7 Lélio Brun ```exception Error of report ``` 9094307a ploc ```(* Module that extract from the DataCycle the set of node that could be inlined ``` ``` to solve the problem. *) ``` ca7ff3f7 Lélio Brun ```module CycleResolution = struct ``` 9094307a ploc ``` (* 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. *) ``` 23ce017b ploc ``` let resolve node partition : call list = ``` 9094307a ploc ``` let partition = ISet.of_list partition in ``` ``` (* Preprocessing calls: associate to each of them the eq.lhs associated *) ``` 333e3a25 ploc ``` let calls_expr = Causality.NodeDep.get_calls (fun _ -> true) node in ``` ``` let eqs, auts = get_node_eqs node in ``` ca7ff3f7 Lélio Brun ``` 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 ``` 9094307a ploc ```end ``` ca7ff3f7 Lélio Brun ```(* Format.fprintf fmt "@[Possible resolution:@ %a@]" pp_resolution ``` ``` resolution*) ``` 9094307a ploc ```let pp_resolution fmt resolution = ``` ca7ff3f7 Lélio Brun ``` fprintf_list ~sep:"@ " ``` ``` (fun fmt (eq, _) -> ``` ``` Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq) ``` ``` fmt resolution ``` ca7e8027 Lélio Brun ```let al_is_solved (_, als) = List.for_all (fun (_, _, status) -> status) als ``` ca7ff3f7 Lélio Brun 23ce017b ploc ```(**********************************************************************) ``` ```(* Functions to access or toggle the local inlining feature of a call *) ``` ```(* expression *) ``` ```(**********************************************************************) ``` 9094307a ploc ```let inline_annotation loc = ``` ca7ff3f7 Lélio Brun ``` ( Inliner.keyword, ``` ``` Corelang.mkeexpr loc (Corelang.mkexpr loc (Expr_const (Const_tag tag_true))) ``` ``` ) ``` 9094307a ploc 264a4844 ploc ```let is_inlining_annot (key, status) = ``` ca7ff3f7 Lélio Brun ``` key = Inliner.keyword ``` ``` && ``` 264a4844 ploc ``` match status.eexpr_qfexpr.expr_desc with ``` ``` | Expr_const (Const_tag tag) when tag = tag_true -> ``` ca7ff3f7 Lélio Brun ``` true ``` 264a4844 ploc ``` | Expr_const (Const_tag tag) when tag = tag_false -> ``` ca7ff3f7 Lélio Brun ``` false ``` ``` | _ -> ``` ``` assert false ``` ```(* expecting true or false value *) ``` 264a4844 ploc ```let is_expr_inlined nd expr = ``` 9094307a ploc ``` match expr.expr_annot with ``` ca7ff3f7 Lélio Brun ``` | None -> ``` ``` false ``` 264a4844 ploc ``` | Some anns -> ( ``` ca7ff3f7 Lélio Brun ``` (* 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) ``` 264a4844 ploc ca7ff3f7 Lélio Brun ```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 ``` 264a4844 ploc 9094307a ploc ```(* Inline the provided expression *) ``` 264a4844 ploc ```let inline_expr node expr = ``` ``` (* Format.eprintf "inlining %a@ @?" Printers.pp_expr expr; *) ``` 9094307a ploc ``` let ann = inline_annotation expr.expr_loc in ``` ca7ff3f7 Lélio Brun ``` let ann = { annots = [ ann ]; annot_loc = expr.expr_loc } in ``` 264a4844 ploc ``` 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 ``` ca7ff3f7 Lélio Brun ```(* Perform the steps of stage1/stage2 to revalidate the schedulability of the ``` ``` program *) ``` 264a4844 ploc ```let fast_stages_processing prog = ``` ca7ff3f7 Lélio Brun ``` Log.report ~level:3 (fun fmt -> ``` ``` Format.fprintf fmt ``` ``` "@[Fast revalidation: normalization + schedulability@ "); ``` 264a4844 ploc ``` Options.verbose_level := !Options.verbose_level - 2; ``` ``` (* Mini stage 1 *) ``` 0d54d8a8 ploc ``` (* Extracting dependencies: fill some table with typing info *) ``` 2200179c ploc ``` (* ignore (Modules.load ~is_header:false prog); REMOVED on 2019/07/16 *) ``` 264a4844 ploc ``` (* 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 ``` ca7ff3f7 Lélio Brun ``` else Compiler_common.check_stateless_decls prog; ``` 264a4844 ploc ``` (* Typing *) ``` ca7ff3f7 Lélio Brun ``` let _ (*computed_types_env*) = ``` ``` Compiler_common.type_decls !Global.type_env prog ``` ``` in ``` 264a4844 ploc ``` (* Clock calculus *) ``` ca7ff3f7 Lélio Brun ``` let _ (*computed_clocks_env*) = ``` ``` Compiler_common.clock_decls !Global.clock_env prog ``` ``` in ``` 264a4844 ploc ``` (* Normalization *) ``` ad4774b0 ploc ``` let params = Backends.get_normalization_params () in ``` ``` let prog = Normalization.normalize_prog params prog in ``` 264a4844 ploc ``` (* Mini stage 2 : Scheduling *) ``` ``` let res = Scheduling.schedule_prog prog in ``` ``` Options.verbose_level := !Options.verbose_level + 2; ``` 9094307a ploc ca7ff3f7 Lélio Brun ``` Log.report ~level:3 (fun fmt -> Format.fprintf fmt "@]@ "); ``` 264a4844 ploc ``` res ``` 9094307a ploc ```(**********************) ``` ```(* Returns a modified node, if possible, and an algebraic_loop report *) ``` 264a4844 ploc ```let rec solving_node max_inlines prog nd existing_al partitions = ``` ``` (* let pp_calls = pp_calls nd in *) ``` 9094307a ploc ``` (* For each partition, we identify the original one *) ``` ca7ff3f7 Lélio Brun ``` let rerun, max_inlines, al = ``` ``` List.fold_left ``` ``` (fun (rerun, _, _) part -> ``` ``` let part_vars = ISet.of_list part in ``` ``` (* Useful functions to filter list of elements *) ``` ``` let match_al (vars, _, _) = ``` ``` 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 (_, expr, _) = ``` ``` 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, _) :: _ -> ``` ``` (* 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 ((_, expr2, _) 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 call -> call, false) calls, ``` ``` false (* Status is nok, LA is unsolved *) ) ``` ``` :: non_matched )) ``` ``` (false, max_inlines, existing_al) ``` ``` partitions ``` 9094307a ploc ``` in ``` ``` (* if partition an already identified al ? *) ``` ``` (* if ISet.of_list partition *) ``` ca7ff3f7 Lélio Brun ``` if rerun && max_inlines > 0 then ( ``` ``` (* At least one partition could be improved: we try to inline the calls and ``` ``` reschedule the node. *) ``` 264a4844 ploc ``` try ``` ca7ff3f7 Lélio Brun ``` Log.report ~level:2 (fun fmt -> ``` ``` Format.fprintf fmt "rescheduling node with new inlined call@ "); ``` 264a4844 ploc ``` let _ = fast_stages_processing prog in ``` ``` (* If everything went up to here, the problem is solved! All associated ``` ca7ff3f7 Lélio Brun ``` alarms are mapped to valid status. *) ``` ``` let al = List.map (fun (v, c, _) -> v, c, true) al in ``` 264a4844 ploc ``` Log.report ~level:2 (fun fmt -> Format.fprintf fmt "AL solved@ "); ``` ca7ff3f7 Lélio Brun ``` 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. *) ``` ad4774b0 ploc ```let clean_al prog : program_t * bool * report = ``` 264a4844 ploc ``` let max_inlines = !Options.al_nb_max in ``` ca7ff3f7 Lélio Brun ``` (* We iterate over each node *) ``` 264a4844 ploc ``` let _, prog, al_list = ``` ca7ff3f7 Lélio Brun ``` 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, [], []) ``` 9094307a ploc ``` in ``` ``` prog, List.for_all al_is_solved al_list, al_list ``` ```(* (ident list * (ident * expr* bool) list * bool) *) ``` ca7e8027 Lélio Brun ```let pp_al nd fmt (partition, calls, _) = ``` 264a4844 ploc ``` let open Format in ``` 9094307a ploc ``` fprintf fmt "@["; ``` ``` fprintf fmt "variables in the alg. loop: @[%a@]@ " ``` ca7ff3f7 Lélio Brun ``` (fprintf_list ~sep:",@ " pp_print_string) ``` ``` partition; ``` 9094307a ploc ``` fprintf fmt "@ involved node calls: @[%a@]@ " ``` ca7ff3f7 Lélio Brun ``` (fprintf_list ~sep:",@ " (fun fmt ((funid, expr, _), status) -> ``` ``` fprintf fmt "%s" funid; ``` ``` if status && is_expr_inlined nd expr then ``` ``` fprintf fmt " (inlining it solves the alg. loop)")) ``` ``` calls; ``` 9094307a ploc ``` fprintf fmt "@]" ``` ca7ff3f7 Lélio Brun ```(* 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 *) ``` 9094307a ploc ```let pp_report fmt report = ``` 264a4844 ploc ``` let open Format in ``` 9094307a ploc ``` fprintf_list ~sep:"@." ``` ca7e8027 Lélio Brun ``` (fun _ (nd, als) -> ``` ca7ff3f7 Lélio Brun ``` let top = Corelang.node_from_name nd.node_id in ``` 264a4844 ploc ``` let pp = ``` ca7ff3f7 Lélio Brun ``` 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 *) ``` 264a4844 ploc ``` in ``` ca7ff3f7 Lélio Brun ``` 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; ``` 9094307a ploc ``` fprintf fmt "@." ``` 264a4844 ploc ```let analyze cpt prog = ``` ``` Log.report ~level:1 (fun fmt -> ``` ca7ff3f7 Lélio Brun ``` Format.fprintf fmt "@[Algebraic loop detected: "; ``` ``` if !Options.solve_al then Format.fprintf fmt "solving mode actived"; ``` ``` Format.fprintf fmt "@ "); ``` 9094307a ploc ``` let prog, status_ok, report = clean_al prog in ``` ca7ff3f7 Lélio Brun 264a4844 ploc ``` let res = ``` ca7ff3f7 Lélio Brun ``` 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 *) ``` 264a4844 ploc ``` else ( ``` ca7ff3f7 Lélio Brun ``` (* We stop with unresolved AL *) ``` ``` (* TODO create a report *) ``` 264a4844 ploc ``` (* Printing the report on stderr *) ``` ``` Format.eprintf "%a" pp_report report; ``` ca7ff3f7 Lélio Brun ``` raise (Error.Error (Location.dummy_loc, Error.AlgebraicLoop))) ``` 264a4844 ploc ``` in ``` ``` (* Printing the report on stderr *) ``` ``` Format.eprintf "%a" pp_report report; ``` ``` res ``` ca7ff3f7 Lélio Brun ```let analyze prog = analyze !Options.al_nb_max prog ```