CristalCaveGem » LustreC

(* 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

   propagated fur future processing Otherwise the compilation stops *)

   ie

   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 *)

exception Error of report

module CycleResolution = struct

    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

(* Format.fprintf fmt "@[<v 2>Possible resolution:@ %a@]" pp_resolution

   resolution*)

  fprintf_list ~sep:"@ "

    (fun fmt (eq, _) ->

      Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq)

    fmt resolution

  ( Inliner.keyword,

    Corelang.mkeexpr loc (Corelang.mkexpr loc (Expr_const (Const_tag tag_true)))

  )

  key = Inliner.keyword

  &&

    true

    false

  | _ ->

    assert false

(* expecting true or false value *)

  | None ->

    false

    (* 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

  let ann = { annots = [ ann ]; annot_loc = expr.expr_loc } in

(* Perform the steps of stage1/stage2 to revalidate the schedulability of the

   program *)

  Log.report ~level:3 (fun fmt ->

      Format.fprintf fmt

        "@[<v 2>Fast revalidation: normalization + schedulability@ ");

  else Compiler_common.check_stateless_decls prog;

  let _ (*computed_types_env*) =

    Compiler_common.type_decls !Global.type_env prog

  in

  let _ (*computed_clocks_env*) =

    Compiler_common.clock_decls !Global.clock_env prog

  in

  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "@]@ ");

  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: @[<v 0>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

  if rerun && max_inlines > 0 then (

    (* At least one partition could be improved: we try to inline the calls and

       reschedule the node. *)

      Log.report ~level:2 (fun fmt ->

          Format.fprintf fmt "rescheduling node with new inlined call@ ");

         alarms are mapped to valid status. *)

      let al = List.map (fun (v, c, _) -> v, c, true) al in

      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. *)

  (* We iterate over each node *)

    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 "@[<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 ->

            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, [], [])

    (fprintf_list ~sep:",@ " pp_print_string)

    partition;

    (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;

(* 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 top = Corelang.node_from_name nd.node_id in

        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 *)

      pp top.top_decl_loc (fun fmt ->

          fprintf fmt "algebraic loop in node %s: {@[<v 0>%a@]}" nd.node_id

            (fprintf_list ~sep:"@ " (pp_al nd))

            als))

    fmt report;

      Format.fprintf fmt "@[<v 2>Algebraic loop detected: ";

      if !Options.solve_al then Format.fprintf fmt "solving mode actived";

      Format.fprintf fmt "@ ");

    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 *)

      (* We stop with unresolved AL *)

      (* TODO create a report *)

      raise (Error.Error (Location.dummy_loc, Error.AlgebraicLoop)))

let analyze prog = analyze !Options.al_nb_max prog