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

   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

open Utils

(* An single algebraic loop is defined (partition, node calls, inlined, status)

   1. the list of variables in the loop, ident list

   3. a status whether the inlining is enough bool *)

(* fun id, expression, and containing equation *)

type algebraic_loop = ident list * (call * bool) list * bool

(* Module that extract from the DataCycle the set of node that could be inlined

   to solve the problem. *)

     the cycle, we store it for future possible inline. *)

    (* Preprocessing calls: associate to each of them the eq.lhs associated *)

    let eqs, auts = get_node_eqs node in

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

   resolution*)

let pp_resolution fmt resolution =

    (fun fmt (eq, _) ->

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

    fmt resolution

(* Functions to access or toggle the local inlining feature of a call *)

(* expression                                                         *)

(**********************************************************************)

let inline_annotation loc =

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

  )

  &&

  | Expr_const (Const_tag tag) when tag = tag_true ->

  | _ ->

    assert false

(* expecting true or false value *)

    false

       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)

  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

  (* Format.eprintf "inlining %a@ @?" Printers.pp_expr expr; *)

  (* assert (is_expr_inlined node res); *)

  (* Format.eprintf "Is expression inlined? %b@." (is_expr_inlined node res); *)

  res

   program *)

      Format.fprintf fmt

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

  (* Mini stage 1 *)

  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

    Compiler_common.type_decls !Global.type_env prog

  in

    Compiler_common.clock_decls !Global.clock_env prog

  in

  let prog = Normalization.normalize_prog params prog in

  let res = Scheduling.schedule_prog prog in

  Options.verbose_level := !Options.verbose_level + 2;

(**********************)

(* Returns a modified node, if possible, and an algebraic_loop report *)

  (* let pp_calls = pp_calls nd in *)

    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 partition an already identified al ? *)

  (* if ISet.of_list partition *)

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

       reschedule the node. *)

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

      (* If everything went up to here, the problem is solved! All associated

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

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

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

  prog, List.for_all al_is_solved al_list, al_list

(* (ident list * (ident * expr* bool) list * bool) *)

  fprintf fmt "variables in the alg. loop: @[<hov 0>%a@]@ "

    partition;

         fprintf fmt "%s" funid;

         if status && is_expr_inlined nd expr then

           fprintf fmt " (inlining it solves the alg. loop)"))

    calls;

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

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

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

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

            als))

    fmt report;

let analyze cpt prog =

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

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

      Format.fprintf fmt "@ ");

      try fast_stages_processing prog with _ -> assert false

      (* Should not happen since the error has been catched already *)

      (* TODO create a report *)

      Format.eprintf "%a" pp_report report;

  (* Printing the report on stderr *)

  Format.eprintf "%a" pp_report report;

  res

let analyze prog = analyze !Options.al_nb_max prog