Module FullLoopbounds

Require Import Bool.
Require Import BinPos.
Require Import List.
Require Import TheoryList.
Require Import Arith.
Require Import Ndec.

Require Import Errors.
Require Import AST.
Require Import Globalenvs.
Require Import RTL.
Require Import Maps.
Require Import Registers.
Require Import Op.
Require Import Coqlib.

Require Import UtilTacs.
Require Import UtilBase.
Require Import UtilLemmas.
Require Import VarsUseDef.
Require Import RTLWfFunction.
Require Import RTLPaths.
Require Import DLib.
Require Import SliceObs.
Require Import SliceRelVar.
Require Import SliceScopeExits.
Require Import Scope.
Require Import ValueAnalysis.
Require Import SliceGen.
Require Import LocalBounds.
Require Import GlobalBounds.
Require Import WCETSlice.

Open Scope error_monad_scope.

Record debug_f := mkdf {
  df_header : node;
  df_vanalysis : node -> var -> res interval;
  df_int_vars : res (list var);
  df_of : obs_function;
  df_tf : function;
  df_lb : res Z
}.

Definition def_va (n : node) (x : var) : res interval := Error (MSG "def_va: undefined" :: nil).
Definition def_iv : res (list var) := Error (MSG "def_iv: undefined" :: nil).
Definition def_of : obs_function :=
  mk_of nil (PTree.empty _) 1%positive (PTree.empty _) (fun x => Regset.empty) 1%positive.
Definition def_lb : res Z := OK(-1%Z).
Definition def_df (h : node) (f : function) : debug_f := mkdf h def_va def_iv def_of f def_lb.

Definition debug_env := PMap.t debug_f.

Definition init_denv (f : function) : debug_env := (def_df 1%positive f, PTree.empty _).

Definition set_header (denv : debug_env) (h : node) : debug_env :=
  let df := PMap.get h denv in
  let new_df := mkdf h (df_vanalysis df) (df_int_vars df) (df_of df) (df_tf df) (df_lb df) in
  PMap.set h new_df denv.

Definition set_vanalysis (denv : debug_env) (h : node) (va : node -> var -> res interval) : debug_env :=
  let df := PMap.get h denv in
  let new_df := mkdf (df_header df) va (df_int_vars df) (df_of df) (df_tf df) (df_lb df) in
  PMap.set h new_df denv.

Definition set_int_vars (denv : debug_env) (h : node) (iv : res (list var)) : debug_env :=
  let df := PMap.get h denv in
  let new_df := mkdf (df_header df) (df_vanalysis df) iv (df_of df) (df_tf df) (df_lb df) in
  PMap.set h new_df denv.

Definition set_of (denv : debug_env) (h : node) (of : obs_function) : debug_env :=
  let df := PMap.get h denv in
  let new_df := mkdf (df_header df) (df_vanalysis df) (df_int_vars df) of (df_tf df) (df_lb df) in
  PMap.set h new_df denv.

Definition set_tf (denv : debug_env) (h : node) (tf : function) : debug_env :=
  let df := PMap.get h denv in
  let new_df := mkdf (df_header df) (df_vanalysis df) (df_int_vars df) (df_of df) tf (df_lb df) in
  PMap.set h new_df denv.

Definition set_lb (denv : debug_env) (h : node) (lb : res Z) : debug_env :=
  let df := PMap.get h denv in
  let new_df := mkdf (df_header df) (df_vanalysis df) (df_int_vars df) (df_of df) (df_tf df) lb in
  PMap.set h new_df denv.

Definition local_bound (denv : debug_env) (f : function) (fsc:Scope.family f) (n : node) : (res Z * debug_env) :=
  let denv := set_header denv n in
  if positive_eq_dec n f.(fn_entrypoint) then (OK 1, denv)
  else
    let value_f := value f in
    let denv' := set_vanalysis denv n value_f in
    let scope_n := Scope.scope fsc n in
    let nodes_n := Scope.nodes scope_n in
    let int_vars := build_all_use_and_def f n nodes_n in
    let denv'' := set_int_vars denv' n int_vars in
    (do vars <- int_vars;
     if check_may_not_update_mem f nodes_n && check_all_only_special_builtins f then
        fold_left (fun rprod0 x =>
                     do prod0 <- rprod0;
                   do itv <- value_f n x;
                   let res := (itv_length itv) * prod0 in
                   OK res
                  ) vars (OK 1)
      else Error (MSG ("local_bound failed: memory updates in function") :: nil), denv'')
.


Definition slicer (f : function) (fsc : Scope.family f) (exit_n : node) (reg_vint : node) (l : node) : res { tf:function &
  { tfsc: Scope.family tf & {of : obs_function | exists FOK:slice_function f l fsc exit_n reg_vint = OK (tf, of),
      tfsc = SliceCFG.transf_family FOK }}}.

Definition opt_error {A} (x:option A) (msg:String.string) : res A :=
  match x with
    | Some x => OK x
    | None => Error (MSG msg :: nil)
  end.

Fixpoint bound_rec
         (denv : debug_env) (f:function) (fsc:Scope.family f) (exit_n:node) (reg_vint:reg)
         (fuel:nat) (sc:Scope.t)
         (acc:PTree.t Z) : res ((PTree.t Z) * debug_env) :=
  match fuel with
    | O => (Error (MSG ("bound_rec: not enough fuel") :: nil))
    | S fuel' =>
      let h := Scope.header fsc sc in
      if ptree_mem h acc then (Error (MSG ("bound_rec assert false") :: nil))
      else
        if peq h f.(fn_entrypoint) then
          let acc' := PTree.set h 1 acc in
          let sons := Scope.sons sc in
          fold_left (fun eacc sc' =>
                       do (acc, de_acc) <- eacc;
                     bound_rec de_acc f fsc exit_n reg_vint fuel' sc' acc
                    ) sons (OK (acc', denv))
        else
          let p_h := Scope.header fsc (Scope.parent fsc sc) in
          do slice <- slicer f fsc exit_n reg_vint h;
            let (tf,tfsc') := slice in
            let (tfsc, of') := tfsc' in
            let (of, _) := of' in
            let denv' := set_of denv h of in
            let denv'' := set_tf denv' h tf in
            let (lb, denv''') := local_bound denv'' tf tfsc h in
            let denv'''' := set_lb denv''' h lb in
            match lb with
              | OK local_bound_h =>
                do bound_p <- opt_error (PTree.get p_h acc) "bound_rec: parent not computed yet";
                  let bound_h := (local_bound_h * bound_p)%Z in
                  let acc' := PTree.set h bound_h acc in
                  let sons := Scope.sons sc in
                  fold_left (fun eacc sc' =>
                               do (acc, de_acc) <- eacc;
                             bound_rec de_acc f fsc exit_n reg_vint fuel' sc' acc) sons (OK (acc', denv''''))
              | Error _ => OK (acc, denv'''')
            end
  end.

Definition full_bounds (f: function) : res ((node -> option Z) * debug_env) :=
  match Scope.build_family f with
    | Some fsc =>
      let main_sc := Scope.scope fsc f.(fn_entrypoint) in
      let all_sc := Scope.elements fsc in
      let res := do (exit_n, reg_vint) <- check_wf f;
                do (bound_headers, denv') <-
                   bound_rec (init_denv f) f fsc exit_n reg_vint (List.length all_sc) main_sc (PTree.empty _);
                OK (fun n =>
                      let h := Scope.header fsc (Scope.scope fsc n) in
                      PTree.get h bound_headers, denv')
      in res
    | None => Error (MSG ("full_bounds: build_scope failed ") :: nil)
  end.