Module SSAfastliveutils

Require Import Bool.
Require Import List. Import ListNotations.
Require Import Sorting.
Require Import OrdersEx.
Require Import Relation_Operators.

Require Import Coqlib.
Require Import AST.
Require Import Maps.
Require Import Utils.
Require Import TrMaps2.
Require Import Kildall.
Require Import KildallComp.
Require Import SSA.
Require Import SSAutils.


Lemma fold_invariant :
  forall {A B} (f : A -> B -> A) l a (P:A->Prop),
  P a ->
  (forall x t, In x l -> P t -> P (f t x)) ->
  P (fold_left f l a).

Lemma fold_becomes_true_growing :
  forall {A B : Type} (f : A -> B -> A) l a (P : A -> Prop),
  Exists (fun b => forall a, P (f a b)) l ->
  forall (f_growing : forall x t, In x l -> P t -> P (f t x)),
  P (List.fold_left f l a).

Lemma fold_becomes_true_growing_with_invariant :
  forall {A B : Type} (f : A -> B -> A) l a (P P0 : A -> Prop),
  P0 a ->
  (forall x t, In x l -> P0 t -> P0 (f t x)) ->
  Exists (fun b => forall a, P0 a -> P (f a b)) l ->
  forall (f_growing : forall x t, In x l -> P0 t -> P t -> P (f t x)),
  P (List.fold_left f l a).



Definition option_union (a b : option unit) : option unit :=
  match a with
  | None => b
  | Some tt => Some tt
  end.

Lemma union_strict_correct : forall m1 m2 x,
  (PTree.combine_union_strict option_union m1 m2) ! x = Some tt
  <-> m1 ! x = Some tt \/ m2 ! x = Some tt.

Lemma union_strict_wf : forall m1 m2,
  PTree.pt_wf m1 -> PTree.pt_wf m2 ->
  PTree.pt_wf (PTree.combine_union_strict option_union m1 m2).

Definition option_diff (a b : option unit) : option unit :=
  match b with
  | None => a
  | Some _ => None
  end.

Lemma diff_correct : forall m1 m2 x,
  (PTree.combine_diff option_diff m1 m2) ! x = Some tt
  <-> m1 ! x = Some tt /\ m2 ! x = None.



Definition is_included '(a, b) '(c, d) :=
  (c <= a)%positive /\ (b <= d)%positive.

Lemma is_included_trans : forall a b c d e f,
  is_included (a, b) (c, d) ->
  is_included (c, d) (e, f) ->
  is_included (a, b) (e, f).

Lemma is_included_dec : forall a b c d,
  is_included (a, b) (c, d) \/
  ~ is_included (a, b) (c, d).

Definition test_is_included '(a, b) '(c, d) :=
  Pos.leb c a && Pos.leb b d.

Lemma test_is_included_spec : forall a b c d,
  test_is_included (a, b) (c, d) = true <-> is_included (a, b) (c, d).

Definition can_reach r (c:PTree.t (PTree.t unit)) u v :=
  match r ! v with
  | None => false
  | Some i_v =>
    match c ! u with
    | None => false
    | Some set =>
      PTree.fold (fun b w _ =>
        b || match r ! w with
             | None => false
             | Some i_w => test_is_included i_v i_w
             end
      ) set false
    end
  end.



Module SortWithIndex (X : Orders.UsualOrderedType).

  Section withIndex.

    Context {A : Type}.
    Context (index : A -> X.t).

    Fixpoint merge (l1 l2 : list (A*X.t)) :=
      let fix merge_aux l2 :=
        match l1, l2 with
        | [], _ => l2
        | _, [] => l1
        | (_, n1) as a1::l1', (_, n2) as a2::l2' =>
            match X.compare n1 n2 with
            | Eq => merge_aux l2'
            | Lt => a1 :: merge l1' l2
            | Gt => a2 :: merge_aux l2'
            end
        end
      in merge_aux l2.

    Fixpoint merge_list_to_stack stack l :=
      match stack with
      | [] => [Some l]
      | None :: stack' => Some l :: stack'
      | Some l' :: stack' => None :: merge_list_to_stack stack' (merge l' l)
      end.

    Fixpoint merge_stack stack :=
      match stack with
      | [] => []
      | None :: stack' => merge_stack stack'
      | Some l :: stack' => merge l (merge_stack stack')
      end.

    Fixpoint iter_merge stack l :=
      match l with
      | [] => merge_stack stack
      | a::l' => iter_merge (merge_list_to_stack stack [(a, index a)]) l'
      end.

    Definition sort_aux := iter_merge [].
    Definition sort l := List.map fst (sort_aux l).

    Local Notation Sorted := (LocallySorted (fun '((_, n1) : A * X.t) '(_, n2) => X.lt n1 n2)) (only parsing).

    Fixpoint SortedStack stack :=
      match stack with
      | [] => True
      | None :: stack' => SortedStack stack'
      | Some l :: stack' => Sorted l /\ SortedStack stack'
      end.

    Local Ltac invert H := inversion H; subst; clear H.

    Local Open Scope list_scope.

    Fixpoint flatten_stack (stack : list (option (list (A * X.t)))) :=
      match stack with
      | [] => []
      | None :: stack' => flatten_stack stack'
      | Some l :: stack' => l ++ flatten_stack stack'
      end.

    Lemma Sorted_merge_aux : forall x1 n1 l1 x2 n2 l2,
      Sorted ((x2, n2) :: l2) ->
      exists x3 n3 l3, merge ((x1, n1) :: l1) ((x2, n2) :: l2) = (x3, n3) :: l3
        /\ (X.eq n3 n1 \/ X.eq n3 n2).

    Theorem Sorted_merge : forall l1 l2,
      Sorted l1 -> Sorted l2 -> Sorted (merge l1 l2).

    Theorem incl_merge : forall l1 l2, incl (merge l1 l2) (l1++l2).

    Theorem incl_merge_2 : forall l1 l2 x n,
      In (x, n) (l1 ++ l2) -> exists y, In (y, n) (merge l1 l2).

    Theorem incl_merge_2_inj : forall l1 l2
      (number_inj : forall x1 x2 n, In (x1, n) l1 -> In (x2, n) l2 -> x1 = x2),
      incl (l1 ++ l2) (merge l1 l2).

    Theorem Sorted_merge_list_to_stack : forall stack l,
      SortedStack stack -> Sorted l -> SortedStack (merge_list_to_stack stack l).

    Theorem incl_merge_list_to_stack : forall stack l,
      incl (flatten_stack (merge_list_to_stack stack l)) (l ++ flatten_stack stack).

    Theorem incl_merge_list_to_stack_2 : forall stack l x n,
      In (x, n) (l ++ flatten_stack stack) ->
      exists y, In (y, n) (flatten_stack (merge_list_to_stack stack l)).

    Theorem incl_merge_list_to_stack_2_inj : forall stack l
      (number_inj : forall x1 x2 n, In (x1, n) (l ++ flatten_stack stack) -> In (x2, n) (l ++ flatten_stack stack) -> x1 = x2),
      incl (l ++ flatten_stack stack) (flatten_stack (merge_list_to_stack stack l)).

    Theorem Sorted_merge_stack : forall stack,
      SortedStack stack -> Sorted (merge_stack stack).

    Theorem incl_merge_stack : forall stack,
      incl (merge_stack stack) (flatten_stack stack).

    Theorem incl_merge_stack_2 : forall stack x n,
      In (x, n) (flatten_stack stack) ->
      exists y, In (y, n) (merge_stack stack).

    Theorem incl_merge_stack_2_inj : forall stack
      (number_inj : forall x1 x2 n, In (x1, n) (flatten_stack stack) ->
        In (x2, n) (flatten_stack stack) -> x1 = x2),
      incl (flatten_stack stack) (merge_stack stack).

    Theorem Sorted_iter_merge : forall stack l,
      SortedStack stack -> Sorted (iter_merge stack l).

    Theorem incl_iter_merge : forall l stack,
      incl (iter_merge stack l)
        (flatten_stack stack ++ List.map (fun a => (a, index a)) l).

    Theorem incl_iter_merge_2 : forall l stack x n,
      In (x, n) (flatten_stack stack ++ List.map (fun a => (a, index a)) l) ->
      exists y, In (y, n) (iter_merge stack l).

    Theorem incl_iter_merge_2_inj : forall l stack
      (number_inj : forall x1 x2 n,
        In (x1, n) (flatten_stack stack ++ List.map (fun a => (a, index a)) l) ->
        In (x2, n) (flatten_stack stack ++List.map (fun a => (a, index a)) l) -> x1 = x2),
      incl (flatten_stack stack ++ List.map (fun a => (a, index a)) l)
        (iter_merge stack l).

    Theorem Sorted_sort_aux : forall l, Sorted (sort_aux l).

    Corollary LocallySorted_sort_aux : forall l,
      Sorted.Sorted (fun '(_, n1) '(_, n2) => X.lt n1 n2) (sort_aux l).

    Theorem incl_sort_aux : forall l,
      incl (sort_aux l) (List.map (fun a => (a, index a)) l).

    Theorem incl_sort_aux_2 : forall l x n,
      In (x, n) (List.map (fun a => (a, index a)) l) ->
      exists y, In (y, n) (sort_aux l).

    Theorem incl_sort_aux_2_inj : forall l
      (number_inj : forall x1 x2 n,
        In (x1, n) (List.map (fun a => (a, index a)) l) ->
        In (x2, n) (List.map (fun a => (a, index a)) l) -> x1 = x2),
      incl (List.map (fun a => (a, index a)) l) (sort_aux l).

    Corollary StronglySorted_sort_aux : forall l,
      StronglySorted (fun '(_, n1) '(_, n2) => X.lt n1 n2) (sort_aux l).

    Theorem Sorted_sort : forall l,
      LocallySorted (fun a b => X.lt (index a) (index b)) (sort l).

    Corollary LocallySorted_sort : forall l,
      Sorted.Sorted (fun a b => X.lt (index a) (index b)) (sort l).

    Theorem incl_sort : forall l,
      incl (sort l) l.

    Theorem incl_sort_2 : forall l x,
      In x l ->
      exists y, In y (sort l) /\ index y = index x.

    Theorem incl_sort_2_nearly_inj : forall l wrong x
      (number_nearly_inj : forall a b,
        In a l -> In b l -> index a = index b -> a = b \/ In (index a) wrong),
      In x l -> ~ In (index x) wrong -> In x (sort l).

    Theorem incl_sort_2_inj : forall l
      (number_inj : forall a b,
        In a l -> In b l -> index a = index b -> a = b),
      incl l (sort l).

    Corollary StronglySorted_sort : forall l,
      StronglySorted (fun a b => X.lt (index a) (index b)) (sort l).

  End withIndex.

End SortWithIndex.

Module PosSortWithIndex := SortWithIndex OrdersEx.Positive_as_OT.
Module ZSortWithIndex := SortWithIndex Z.



Definition itv_strict_incl (i1 i2:itv) : bool :=
  if Z_lt_dec i2.(pre) i1.(pre) then
    if Z_le_dec i1.(post) i2.(post) then true
    else false
  else false.

Definition itv_strict_Incl i1 i2 :=
  i2.(pre) < i1.(pre) /\ i1.(post) <= i2.(post).

Lemma itv_strict_incl_spec : forall i1 i2,
  itv_strict_incl i1 i2 = true <-> itv_strict_Incl i1 i2.

Definition is_strict_ancestor (dom : PTree.t itv) (n1 n2:node) : bool :=
  match dom ! n1, dom ! n2 with
    | Some itv1, Some itv2 => itv_strict_incl itv2 itv1
    | _, _ => false
  end.

Definition sdom_test f := is_strict_ancestor f.(fn_dom).

Lemma sdom_test_correct : forall f (wf : wf_ssa_function f) n d,
  reached f n -> sdom_test f d n = true <-> sdom f d n.




Definition du_chain := P2Map.t (list node).

Construction

Definition regs_used_by (i : instruction) : list reg :=
 match i with
    | Iop _ l _ _ => l
    | Iload _ _ l _ _ => l
    | Istore _ _ l src _ => src::l
    | Icall _ ros l _ _
    | Itailcall _ ros l =>
      match ros with
        | inl r => r :: l
        | inr _ => l
      end
    | Ibuiltin _ l _ _ => (params_of_builtin_args l)
    | Icond _ l _ _ => l
    | Ijumptable r _ => r :: nil
    | Ireturn (Some r) => r :: nil
    | _ => nil
  end.

Lemma regs_used_by_correct : forall f pc i r,
  f.(fn_code) ! pc = Some i ->
  use_code f r pc ->
  In r (regs_used_by i).

Lemma regs_used_by_complete : forall f pc i r,
  f.(fn_code) ! pc = Some i ->
  In r (regs_used_by i) ->
  use_code f r pc.

Definition handle_reg_list (duc: du_chain) (pc : node) (rs: list reg) :=
  List.fold_left (fun u r => P2Map.set r (pc :: u #2 r) u) rs duc.

Lemma handle_reg_list_correct_1 : forall duc pc rs r pc',
  In pc' (duc #2 r) ->
  In pc' ((handle_reg_list duc pc rs) #2 r).

Lemma handle_reg_list_correct_2 : forall duc pc rs r,
  In r rs ->
  In pc ((handle_reg_list duc pc rs) #2 r).

Lemma handle_reg_list_complete_1 : forall duc pc rs r,
  In pc ((handle_reg_list duc pc rs) #2 r) ->
  ~ In pc (duc #2 r) ->
  In r rs.

Lemma handle_reg_list_complete_2 : forall duc pc rs r pc',
  In pc' ((handle_reg_list duc pc rs) #2 r) ->
  pc' <> pc ->
  In pc' (duc #2 r).

Definition def_use_1 duc c :=
  PTree.fold (fun u pc i => handle_reg_list u pc (regs_used_by i)) c duc.

Lemma def_use_1_correct_1 : forall duc c r pc,
  In pc (duc #2 r) ->
  In pc ((def_use_1 duc c) #2 r).

Lemma def_use_1_correct_2 : forall f duc r pc,
  use_code f r pc ->
  In pc ((def_use_1 duc f.(fn_code)) #2 r).

Lemma def_use_1_complete : forall f duc r pc,
  In pc ((def_use_1 duc f.(fn_code)) #2 r) ->
  ~ In pc (duc #2 r) ->
  use_code f r pc.

Definition handle_phi_block_k (duc:du_chain) k pc pb :=
  List.fold_left (fun u pi =>
    match pi with
    | Iphi args _ =>
      match nth_error args k with
      | None => u
      | Some r => P2Map.set r (pc :: u #2 r) u
      end
    end) pb duc.

Lemma handle_phi_block_k_correct_1 : forall duc k pc pb r pc',
  In pc' (duc #2 r) ->
  In pc' ((handle_phi_block_k duc k pc pb) #2 r).

Lemma handle_phi_block_k_correct_2 : forall duc k pc pb args dst r,
  In (Iphi args dst) pb ->
  nth_error args k = Some r ->
  In pc ((handle_phi_block_k duc k pc pb) #2 r).

Lemma handle_phi_block_k_complete_1 : forall duc k pc pb r,
  In pc ((handle_phi_block_k duc k pc pb) #2 r) ->
  ~ In pc (duc #2 r) ->
  exists args dst,
    In (Iphi args dst) pb /\ nth_error args k = Some r.

Section fold_left2.

Context {A B C : Type}.
Context (f : A -> B -> C -> A).

Fixpoint fold_left2 (l1 : list B) (l2 : list C) a :=
  match l1, l2 with
  | [], _ => a
  | _, [] => a
  | b :: l1, c :: l2 => fold_left2 l1 l2 (f a b c)
  end.

Lemma fold_left2_invariant_nth : forall l1 l2 a (P:A->Prop),
  P a ->
  (forall k b c t,
    nth_error l1 k = Some b ->
    nth_error l2 k = Some c ->
    P t -> P (f t b c)) ->
  P (fold_left2 l1 l2 a).

Lemma fold_left2_invariant : forall l1 l2 a (P:A->Prop),
  P a ->
  (forall b c t, In b l1 -> In c l2 -> P t -> P (f t b c)) ->
  P (fold_left2 l1 l2 a).

Lemma fold_left2_app : forall l11 l12 l21 l22 a,
  List.length l11 = List.length l21 ->
  fold_left2 (l11 ++ l12) (l21 ++ l22) a
  = fold_left2 l12 l22 (fold_left2 l11 l21 a).

Lemma fold_left2_becomes_true_growing :
  forall l1 l2 a (P : A -> Prop) k b c,
  nth_error l1 k = Some b ->
  nth_error l2 k = Some c ->
  (forall a, P (f a b c)) ->
  forall (f_growing : forall b c t, In b l1 -> In c l2 -> P t -> P (f t b c)),
  P (fold_left2 l1 l2 a).

End fold_left2.

Definition handle_phi_instr (duc : du_chain) preds pi :=
  match pi with
  | Iphi args _ =>
    fold_left2 (fun c pc arg => P2Map.set arg (pc :: c #2 arg) c) preds args duc
  end.

Lemma handle_phi_instr_correct_1 : forall duc preds pi r pc,
  In pc (duc #2 r) ->
  In pc ((handle_phi_instr duc preds pi) #2 r).

Lemma handle_phi_instr_correct_2 : forall duc preds args dst k r pc,
  nth_error preds k = Some pc ->
  nth_error args k = Some r ->
  In pc ((handle_phi_instr duc preds (Iphi args dst)) #2 r).

Lemma handle_phi_instr_complete : forall duc preds args dst r pc,
  In pc ((handle_phi_instr duc preds (Iphi args dst)) #2 r) ->
  ~ In pc (duc #2 r) ->
  exists k, nth_error preds k = Some pc /\ nth_error args k = Some r.

Definition handle_phi_block (duc : du_chain) preds (pb : phiblock) :=
    fold_left (fun u pi => handle_phi_instr u preds pi) pb duc.

Lemma handle_phi_block_correct_1 : forall duc preds pb r pc,
  In pc (duc #2 r) ->
  In pc ((handle_phi_block duc preds pb) #2 r).

Lemma handle_phi_block_correct_2 : forall duc preds pb args dst k r pc,
  In (Iphi args dst) pb ->
  nth_error args k = Some r ->
  nth_error preds k = Some pc ->
  In pc ((handle_phi_block duc preds pb) #2 r).

Lemma handle_phi_block_complete : forall duc preds pb r pc,
  In pc ((handle_phi_block duc preds pb) #2 r) ->
  ~ In pc (duc #2 r) ->
  exists args dst k,
    In (Iphi args dst) pb /\
    nth_error preds k = Some pc /\
    nth_error args k = Some r.

Definition def_use_2 duc c phic :=
  let preds := make_predecessors c successors_instr in
  PTree.fold (fun u pc pb =>
    match preds ! pc with
    | None => u
    | Some preds => handle_phi_block u preds pb
    end) phic duc.

Lemma def_use_2_correct_1 : forall duc c phic r pc,
  In pc (duc #2 r) ->
  In pc ((def_use_2 duc c phic) #2 r).

Lemma def_use_2_correct_2 : forall f (wf : wf_ssa_function f) duc r pc,
  use_phicode f r pc ->
  In pc ((def_use_2 duc f.(fn_code) f.(fn_phicode)) #2 r).

Lemma make_predecessors_NoDup : forall f (wf : wf_ssa_function f) pc,
  NoDup ((make_predecessors f.(fn_code) successors_instr) !!! pc).

Lemma def_use_2_complete : forall f (wf : wf_ssa_function f) duc r pc,
  In pc ((def_use_2 duc f.(fn_code) f.(fn_phicode)) #2 r) ->
  ~ In pc (duc #2 r) ->
  use_phicode f r pc.

Definition make_du_chain f : du_chain :=
  let u := def_use_1 (P2Map.init nil) (fn_code f) in
  def_use_2 u f.(fn_code) f.(fn_phicode).

Lemma make_du_chain_correct : forall f (wf : wf_ssa_function f) r pc,
  use f r pc ->
  In pc ((make_du_chain f) #2 r).

Lemma make_du_chain_complete : forall f (wf : wf_ssa_function f) r pc,
  In pc ((make_du_chain f) #2 r) ->
  use f r pc.




Definition defined_var ins :=
  match ins with
  | Iop _ _ r _ => Some r
  | Iload _ _ _ r _ => Some r
  | Icall _ _ _ r _ => Some r
  | Ibuiltin _ _ (BR r) _ => Some r
  | _ => None
  end.

Definition compute_code_def (f : function) : P2Tree.t node -> P2Tree.t node :=
  PTree.fold
    (fun acc pc ins =>
      match defined_var ins with
      | Some r => P2Tree.set r pc acc
      | None => acc
      end)
    (fn_code f).

Definition compute_phi_def (f : function) : P2Tree.t node -> P2Tree.t node :=
  PTree.fold
   (fun acc pc phib =>
     fold_left
       (fun acc phi =>
       match phi with
       | Iphi args dst =>
           P2Tree.set dst pc acc
       end)
       phib acc)
   (fn_phicode f).


Definition get_all_def f :=
  let defs := P2Tree.empty node in
  let defs := compute_code_def f defs in
  let defs := compute_phi_def f defs in
  defs.

Definition compute_def (f : function) all_defs :=
  fun r =>
    match all_defs !2 r with
    | Some d => d
    | None => fn_entrypoint f
    end.

Lemma assigned_code_spec_defined_var : forall f d r,
  assigned_code_spec f.(fn_code) d r ->
  exists i, f.(fn_code) ! d = Some i /\ defined_var i = Some r.

Lemma defined_var_assigned_code_spec : forall f d i r,
  f.(fn_code) ! d = Some i -> defined_var i = Some r ->
  assigned_code_spec f.(fn_code) d r.

Lemma compute_code_def_correct_1 : forall f (wf : wf_ssa_function f) defs r,
  (forall pc, ~ assigned_code_spec f.(fn_code) pc r) ->
  (compute_code_def f defs) !2 r = defs !2 r.

Lemma compute_code_def_correct_2 : forall f (wf : wf_ssa_function f) defs r d,
  assigned_code_spec f.(fn_code) d r ->
  (compute_code_def f defs) !2 r = Some d.

Lemma compute_code_def_complete : forall f (wf : wf_ssa_function f) defs r d,
  (compute_code_def f defs) !2 r = Some d ->
  defs !2 r = None ->
  assigned_code_spec f.(fn_code) d r.

Lemma compute_phi_def_correct_1 : forall f (wf : wf_ssa_function f) defs r,
  (forall pc, ~ assigned_phi_spec f.(fn_phicode) pc r) ->
  (compute_phi_def f defs) !2 r = defs !2 r.

Lemma compute_phi_def_correct_2 : forall f (wf : wf_ssa_function f) defs r d,
  assigned_phi_spec f.(fn_phicode) d r ->
  (compute_phi_def f defs) !2 r = Some d.

Lemma compute_phi_def_complete : forall f (wf : wf_ssa_function f) defs r d,
  (compute_phi_def f defs) !2 r = Some d ->
  defs !2 r = None ->
  assigned_phi_spec f.(fn_phicode) d r.

Lemma compute_def_correct :
  forall f (wf : wf_ssa_function f) r d,
  def f r d ->
  compute_def f (get_all_def f) r = d.

Lemma compute_def_complete : forall f (wf : wf_ssa_function f) r d
  (USE: exists pc, use f r pc),
  compute_def f (get_all_def f) r = d ->
  def f r d.



Definition collect_variables f :=
  let defs := all_def f.(fn_code) f.(fn_phicode) in
  let uses := all_uses f.(fn_code) f.(fn_phicode) in
  let params :=
    List.fold_left (fun acc x => SSARegSet.add x acc) f.(fn_params) SSARegSet.empty
  in
  SSARegSet.union (SSARegSet.union defs uses) params.

Definition ignore2 {A B} (x : A) (y : B) := x.



Lemma clos_refl_trans_clos_trans : forall {A} (R : A -> A -> Prop) x y,
  clos_refl_trans _ R x y <-> x = y \/ clos_trans _ R x y.