Module SSAutils

Require Import Coqlib.
Require Import Maps.
Require Import Maps2.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Events.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import Floats.
Require Import Kildall.
Require Import KildallComp.
Require Import SSA.
Require Import Utils.
Require Import Relation_Operators.
Require Import Classical.
Require Import OrderedType.
Require Import Ordered.
Require Import FSets.
Require Import DLib.
Require FSetAVL.
Unset Allow StrictProp.
    

Utility lemmas about index_pred

Lemma index_pred_some : forall pc t k pc0,
  index_pred t pc0 pc = Some k ->
  (k < length (t!!!pc))%nat.
Proof.

Lemma index_pred_some_nth: forall pc t k pc0,
  index_pred t pc0 pc = Some k ->
  nth_error (t!!!pc) k = Some pc0.
Proof.

Utility lemmas about successors

Lemma successors_instr_succs : forall f pc pc' instr,
(fn_code f) ! pc = Some instr ->
In pc' (successors_instr instr) ->
exists succs, (successors f) ! pc = Some succs /\ In pc' succs .
Proof.

Lemma index_pred_instr_some :
  forall instr pc' f pc ,
    (fn_code f)!pc = Some instr ->
    In pc' (successors_instr instr) ->
    (exists k, index_pred (make_predecessors (fn_code f) successors_instr) pc pc' = Some k).
Proof.

Lemma get_index_cons_succ: forall x xs k y,
    get_index (x::xs) y = Some (Datatypes.S k) -> get_index xs y = Some k.
Proof.

Utility lemmas about wf_ssa_function


Lemma no_assigned_phi_spec_fn_entrypoint: forall f,
  wf_ssa_function f -> forall x,
    ~ assigned_phi_spec (fn_phicode f) (fn_entrypoint f) x.
Proof.


Lemma fn_phiargs: forall f,
  wf_ssa_function f ->
  forall pc block x args pred k,
    (fn_phicode f) ! pc = Some block ->
    In (Iphi args x) block ->
    index_pred (Kildall.make_predecessors (fn_code f) successors_instr) pred pc = Some k ->
    exists arg, nth_error args k = Some arg.
Proof.
  
Lemma fn_phicode_code : forall f,
  wf_ssa_function f ->
  forall pc block,
    (fn_phicode f) ! pc = Some block ->
    exists ins, (fn_code f) ! pc = Some ins.
Proof.

Lemma fn_entrypoint_inv: forall f,
  wf_ssa_function f ->
    (exists i, (f.(fn_code) ! (f.(fn_entrypoint)) = Some i)) /\
    ~ join_point f.(fn_entrypoint) f.
Proof.
  
Lemma fn_code_inv2: forall f,
  wf_ssa_function f ->
  forall jp pc, (join_point jp f) ->
    In jp ((successors f) !!! pc) ->
    f.(fn_code) ! pc = Some (Inop jp).
Proof.
  
Lemma fn_phicode_inv1: forall f,
  wf_ssa_function f ->
  forall phib jp i,
    f.(fn_code) ! jp = Some i ->
    f.(fn_phicode) ! jp = Some phib ->
    join_point jp f.
Proof.
  
Lemma fn_phicode_inv2: forall f,
  wf_ssa_function f ->
  forall jp i,
    join_point jp f ->
    f.(fn_code) ! jp = Some i ->
    exists phib, f.(fn_phicode) ! jp = Some phib.
Proof.

Lemma not_jnp_not_assigned_phi_spec: forall f pc y,
  wf_ssa_function f ->
  ~ join_point pc f ->
  ~ assigned_phi_spec (fn_phicode f) pc y.
Proof.

Lemma ssa_def_dom_use : forall f,
  wf_ssa_function f ->
  forall x u d, use f x u -> def f x d -> dom f d u.
Proof.

Lemma ssa_use_exists_def : forall f,
  wf_ssa_function f ->
  forall x u,
  use f x u -> exists d, def f x d.
Proof.

Lemma wf_ssa_reached : forall f,
  wf_ssa_function f ->
  forall pc ins,
  (fn_code f) ! pc = Some ins ->
  reached f pc.
Proof.
Global Hint Resolve wf_ssa_reached: core.

Lemma ssa_def_use_code_false : forall f,
  wf_ssa_function f ->
  forall x pc,
  use_code f x pc ->
  assigned_code_spec (fn_code f) pc x ->
  False.
Proof.
  
Lemma ssa_not_Inop_not_phi : forall f,
  wf_ssa_function f ->
  forall pc x pc' ins,
  In pc' (successors_instr ins) ->
  (fn_code f) ! pc = Some ins ->
  (forall n, ins <> Inop n) ->
  ~ assigned_phi_spec (fn_phicode f) pc' x.
Proof.

Lemma unique_def_spec_def : forall f x d1 d2
  (HWF: wf_ssa_function f),
  def f x d1 ->
  def f x d2 ->
  d1 <> d2 -> False.
Proof.

Lemma def_def_eq : forall f x d1 d2
  (HWF: wf_ssa_function f),
  def f x d1 ->
  def f x d2 ->
  d1 = d2.
Proof.

Ltac def_def f x pc pc' :=
  match goal with
    | [HWF: wf_ssa_function f |- _ ] =>
      (exploit (def_def_eq f x pc pc' HWF); eauto);
      try (econstructor ; eauto);
        try (solve [econstructor ; eauto])
  end.

Require RTL.
Ltac allinv :=
  repeat
    match goal with
      | [ H1: (fn_code ?tf) ! ?pc = Some _ ,
        H2: (fn_code ?tf) ! ?pc = Some _ |- _ ] =>
      rewrite H1 in H2; inv H2
      | [ H1: (RTL.fn_code ?tf) ! ?pc = Some _ ,
        H2: (RTL.fn_code ?tf) ! ?pc = Some _ |- _ ] =>
      rewrite H1 in H2; inv H2
      | [ H1: (fn_phicode ?tf) ! ?pc = Some _ ,
        H2: (fn_phicode ?tf) ! ?pc = Some _ |- _ ] =>
      rewrite H1 in H2; inv H2
      | [ H1: ?Γ ! ?pc = _ ,
        H2: ?Γ ! ?pc = _ |- _ ] =>
      rewrite H1 in H2; inv H2
      | [ H1: index_pred _ ?pc ?pc' = Some _ ,
        H2: index_pred _ ?pc ?pc' = Some _ |- _ ] =>
      rewrite H1 in H2; inv H2
      | _ => idtac
    end.

Lemma ssa_def_unique : forall f x d1 d2,
  wf_ssa_function f -> def f x d1 -> def f x d2 -> d1 = d2.
Proof.

Lemma assigned_code_and_phi: forall f,
  wf_ssa_function f -> forall r pc pc',
    assigned_code_spec (fn_code f) pc r ->
    assigned_phi_spec (fn_phicode f) pc' r -> False.
Proof.

Lemma assigned_code_unique : forall f,
  wf_ssa_function f -> forall r pc pc',
    assigned_code_spec (fn_code f) pc r ->
    assigned_code_spec (fn_code f) pc' r -> pc=pc'.
Proof.

Lemma assigned_phi_spec_join_point : forall f x pc,
  wf_ssa_function f ->
  assigned_phi_spec (fn_phicode f) pc x ->
  join_point pc f.
Proof.

Lemma wf_ssa_use_and_def_same_pc : forall f x pc,
  wf_ssa_function f ->
  use f x pc ->
  def f x pc ->
  assigned_phi_spec (fn_phicode f) pc x \/ ext_params f x.
Proof.

Properties and more lemmas about well-formed SSA functions

Section WF_SSA_PROP.

Variable f: function.
Hypothesis HWF : wf_ssa_function f.
Hint Resolve HWF: core.

Lemma elim_structural : forall pc pc' instr instr' block,
    (fn_code f)! pc = Some instr ->
    (fn_code f)! pc' = Some instr' ->
    (fn_phicode f)!pc' = Some block ->
    In pc' (successors_instr instr) ->
    instr = Inop pc'.
Proof.

Lemma phicode_joinpoint: forall pc block i,
  (fn_code f) ! pc = Some i ->
  (fn_phicode f) ! pc = Some block ->
  join_point pc f.
Proof.

Lemma nophicode_nojoinpoint: forall pc i,
  (fn_code f) ! pc = Some i ->
  (fn_phicode f) ! pc = None ->
  ~ join_point pc f.
Proof.

Lemma join_point_exclusive: forall pc i,
  (fn_code f) ! pc = Some i ->
  ~ join_point pc f \/ join_point pc f.
Proof.


Lemma use_ins_code : forall pc x,
  use f x pc ->
  exists ins, (fn_code f) ! pc = Some ins.
Proof.

Lemma use_reached : forall pc x,
  use f x pc ->
  reached f pc.
Proof.

End WF_SSA_PROP.

Auxiliary semantics for phi-blocks


Lemmas about the sequential semantics of phiblocks
Lemma notin_cons_notin : forall dst block a,
  (forall args, ~ In (Iphi args dst) (a:: block)) ->
  forall args, ~ In (Iphi args dst) block.
Proof.
Global Hint Resolve notin_cons_notin: core.
    
Lemma phi_store_notin_preserved: forall k block rs dst,
  (forall args, ~ (In (Iphi args dst) block)) ->
    (phi_store k block rs)# dst = rs# dst.
Proof.

How to compute the list of registers of a SSA function.

Module SSARegSet := FSetAVL.Make OrderedPositive.

Definition all_def (c:code) (phic: phicode) : SSARegSet.t :=
  PTree.fold
    (fun s _ ins =>
      match ins with
        | Iop op args dst succ => SSARegSet.add dst s
        | Iload chunk addr args dst succ => SSARegSet.add dst s
        | Icall sig fn args dst succ => SSARegSet.add dst s
        | Ibuiltin fn args (BR dst) succ => SSARegSet.add dst s
        | _ => s
      end) c
    (PTree.fold
      (fun s _ phib =>
        List.fold_left
        (fun s (phi:phiinstruction) => let (_,dst) := phi in SSARegSet.add dst s)
        phib s) phic SSARegSet.empty).

Definition param_set (params: list reg) : SSARegSet.t :=
  List.fold_right SSARegSet.add SSARegSet.empty params.

Definition all_uses (c: code) (phic: phicode) : SSARegSet.t :=
  PTree.fold
    (fun s _ ins =>
      match ins with
        | Iop op args dst _ => fold_right SSARegSet.add s args
        | Iload chk adr args dst _ => fold_right SSARegSet.add s args
        | Icond cond args _ _ => fold_right SSARegSet.add s args
        | Ibuiltin ef args dst _ => fold_right SSARegSet.add s (params_of_builtin_args args)
        | Istore chk adr args src _ => fold_right SSARegSet.add s (src::args)
        | Icall sig (inl r) args dst _ => fold_right SSARegSet.add s (r::args)
        | Itailcall sig (inl r) args => fold_right SSARegSet.add s (r::args)
        | Icall sig (inr id) args dst _ => fold_right SSARegSet.add s args
        | Itailcall sig (inr id) args => fold_right SSARegSet.add s args
        | Ijumptable arg tbl => SSARegSet.add arg s
        | Ireturn (Some arg) => SSARegSet.add arg s
        | _ => s
      end) c
    (PTree.fold
      (fun s _ phib =>
        fold_left
        (fun s (phi:phiinstruction) =>
          let (args,dst) := phi in
            fold_right SSARegSet.add s args)
        phib s) phic SSARegSet.empty).

Lemma In_fold_right_add1: forall x l a,
 In x l -> SSARegSet.In x (fold_right SSARegSet.add a l).
Proof.

Lemma In_fold_right_add2: forall x l a,
  SSARegSet.In x a -> SSARegSet.In x (fold_right SSARegSet.add a l).
Proof.

Lemma In_fold_right_add3: forall x l a,
  SSARegSet.In x (fold_right SSARegSet.add a l) -> SSARegSet.In x a \/ In x l.
Proof.

Lemma in_all_uses1: forall x pc code s ins,
  code!pc = Some ins ->
      match ins with
        | Iop op args dst _ => In x args
        | Iload chk adr args dst _ => In x args
        | Icond cond args _ _ => In x args
        | Ibuiltin ef args dst _ => In x (params_of_builtin_args args)
        | Istore chk adr args src _ => In x (src::args)
        | Icall sig (inl r) args dst _ => In x (r::args)
        | Itailcall sig (inl r) args => In x (r::args)
        | Icall sig (inr id) args dst _ => In x args
        | Itailcall sig (inr id) args => In x args
        | Ijumptable arg tbl => x = arg
        | Ireturn (Some arg) => x = arg
        | _ => False
      end ->
  SSARegSet.In x
  (PTree.fold
    (fun s _ ins =>
      match ins with
        | Iop op args dst _ => fold_right SSARegSet.add s args
        | Iload chk adr args dst _ => fold_right SSARegSet.add s args
        | Icond cond args _ _ => fold_right SSARegSet.add s args
        | Ibuiltin ef args dst _ => fold_right SSARegSet.add s (params_of_builtin_args args)
        | Istore chk adr args src _ => fold_right SSARegSet.add s (src::args)
        | Icall sig (inl r) args dst _ => fold_right SSARegSet.add s (r::args)
        | Itailcall sig (inl r) args => fold_right SSARegSet.add s (r::args)
        | Icall sig (inr id) args dst _ => fold_right SSARegSet.add s args
        | Itailcall sig (inr id) args => fold_right SSARegSet.add s args
        | Ijumptable arg tbl => SSARegSet.add arg s
        | Ireturn (Some arg) => SSARegSet.add arg s
        | _ => s
      end) code s).
Proof.

Lemma in_all_uses2: forall x code s,
  SSARegSet.In x s ->
  SSARegSet.In x
  (PTree.fold
    (fun s _ ins =>
      match ins with
        | Iop op args dst _ => fold_right SSARegSet.add s args
        | Iload chk adr args dst _ => fold_right SSARegSet.add s args
        | Icond cond args _ _ => fold_right SSARegSet.add s args
        | Ibuiltin ef args dst _ => fold_right SSARegSet.add s (params_of_builtin_args args)
        | Istore chk adr args src _ => fold_right SSARegSet.add s (src::args)
        | Icall sig (inl r) args dst _ => fold_right SSARegSet.add s (r::args)
        | Itailcall sig (inl r) args => fold_right SSARegSet.add s (r::args)
        | Icall sig (inr id) args dst _ => fold_right SSARegSet.add s args
        | Itailcall sig (inr id) args => fold_right SSARegSet.add s args
        | Ijumptable arg tbl => SSARegSet.add arg s
        | Ireturn (Some arg) => SSARegSet.add arg s
        | _ => s
      end) code s).
Proof.

Lemma in_all_uses3 : forall x code s pc phib args dst,
  code!pc = Some phib ->
  In (Iphi args dst) phib ->
  In x args ->
   SSARegSet.In x
     (PTree.fold
        (fun (s : SSARegSet.t) (_ : positive) (phib : list phiinstruction) =>
         fold_left
           (fun (s0 : SSARegSet.t) (phi : phiinstruction) =>
            let (args, _) := phi in fold_right SSARegSet.add s0 args) phib s)
        code s).
Proof.


Definition ext_params_list (c: code) (phic: phicode) (params: list reg) : list reg :=
  SSARegSet.elements
  (SSARegSet.diff (all_uses c phic)
    (SSARegSet.union (all_def c phic) (param_set params)))
++params.

Lemma In_param_set : forall l x, SSARegSet.In x (param_set l) -> In x l.
Proof.

Lemma use_In_all_usses : forall f x pc,
  use f x pc -> SSARegSet.In x (all_uses (fn_code f) (fn_phicode f)).
Proof.

Lemma In_all_def1: forall x code s,
  SSARegSet.In x
  (PTree.fold
    (fun (s : SSARegSet.t) (_ : positive) (ins : instruction) =>
      match ins with
        | Inop _ => s
        | Iop _ _ dst _ => SSARegSet.add dst s
        | Iload _ _ _ dst _ => SSARegSet.add dst s
        | Istore _ _ _ _ _ => s
        | Icall _ _ _ dst _ => SSARegSet.add dst s
        | Itailcall _ _ _ => s
        | Ibuiltin _ _ (BR dst) _ => SSARegSet.add dst s
        | Ibuiltin _ _ _ _ => s
        | Icond _ _ _ _ => s
        | Ijumptable _ _ => s
        | Ireturn _ => s
      end) code s) ->
  SSARegSet.In x s \/
  exists pc : node, assigned_code_spec code pc x.
Proof.

Lemma In_fold_left_add1 : forall x phib s,
  SSARegSet.In x (fold_left (fun s0 (phi:phiinstruction) => let (_, dst) := phi in SSARegSet.add dst s0) phib s) ->
  SSARegSet.In x s \/ exists args, In (Iphi args x) phib.
Proof.

Lemma In_all_def2: forall x p s,
   SSARegSet.In x
     (PTree.fold
        (fun (s : SSARegSet.t) (_ : positive) (phib : list phiinstruction) =>
         fold_left
           (fun (s0 : SSARegSet.t) (phi : phiinstruction) =>
            let (_, dst) := phi in SSARegSet.add dst s0) phib s) p
        s) ->
     SSARegSet.In x s \/
     exists pc : node, assigned_phi_spec p pc x.
Proof.

Lemma In_all_def : forall f x,
  SSARegSet.In x (all_def (fn_code f) (fn_phicode f)) ->
  (exists pc, assigned_phi_spec (fn_phicode f) pc x)
  \/ (exists pc, assigned_code_spec (fn_code f) pc x).
Proof.

Lemma InA_In : forall x (l:list reg),
  InA (fun a b : OrderedPositive.t => a = b) x l <-> In x l.
Proof.

Lemma ext_params_list_spec : forall f x,
    ext_params f x ->
    In x (ext_params_list (fn_code f) (fn_phicode f) (fn_params f)).
Proof.

Lemma unique_def_elim1: forall f pc pc' x,
  unique_def_spec f ->
  assigned_code_spec (fn_code f) pc x ->
  assigned_phi_spec (fn_phicode f) pc' x ->
  False.
Proof.

  Ltac ssa_def :=
    let eq_pc pc1 pc2 :=
    assert (pc1 = pc2) by (eapply ssa_def_unique; eauto); subst
    in
    match goal with
      | r : reg |- _ =>
            match goal with
               id: def _ r ?x,
               id': def _ r ?y
               |- _ => eq_pc x y ; try clear id'
            end
      | pc1: node,
        pc2: node |- _ =>
            match goal with
                id : def _ ?r pc1,
                id': assigned_phi_spec _ pc2 ?r |- _ =>
                eq_pc pc1 pc2
            end
      | pc1: node,
         pc2: node |- _ =>
            match goal with
                id: assigned_phi_spec _ pc1 ?r,
                id': assigned_phi_spec _ pc2 ?r |- _ =>
                eq_pc pc1 pc2
            end
      | id : _ ! ?pc1 = Some (Iop _ _ ?r _),
        id' : _ ! ?pc2 = Some (Iop _ _ ?r _)
        |- _ =>
        match pc2 with
          | pc1 => fail 1
          | _ => idtac
        end;
          eq_pc pc1 pc2
      | id : _ ! ?pc1 = Some (Iop _ _ ?r _),
        id': def _ ?r ?pc2 |- _ =>
        match pc2 with
          | pc1 => fail 1
          | _ => idtac
        end;
          eq_pc pc1 pc2
      end.

The is_edge predicate

Variant is_edge (tf:SSA.function) : node -> node -> Prop:=
| Edge: forall i j instr,
  (fn_code tf)!i = Some instr ->
  In j (successors_instr instr) ->
  is_edge tf i j.

Lemma is_edge_pred: forall tf i j,
  is_edge tf i j ->
  exists k, index_pred (make_predecessors (fn_code tf) successors_instr) i j = Some k.
Proof.

Lemma pred_is_edge_help: forall tf i j k,
  index_pred (make_predecessors (fn_code tf) successors_instr) i j = Some k ->
  (is_edge tf i j).
Proof.
  
Lemma pred_is_edge: forall tf i j k,
                      index_pred (make_predecessors (fn_code tf) successors_instr) i j = Some k -> is_edge tf i j.
Proof.

Variant ssa_def : Type :=
| SDIop (pc:node)
| SDPhi (pc:node) (idx:nat).

Variant ssa_eq : Type :=
| EqIop (op:operation) (args:list reg) (dst:reg)
| EqPhi (dst:reg) (args:list reg).

Definition ssa_eq_to_dst (eq:ssa_eq) : reg :=
  match eq with
    | EqIop _ _ dst => dst
    | EqPhi dst _ => dst
  end.

Definition get_ssa_eq (f:function) (d:ssa_def) : option ssa_eq :=
  match d with
    | SDIop pc =>
      match (fn_code f)!pc with
        | Some (Iop op args dst _) => Some (EqIop op args dst)
        | _ => None
      end
    | SDPhi pc idx =>
      match (fn_phicode f)!pc with
        | Some phi =>
          match nth_error phi idx with
            | Some (Iphi args dst) => Some (EqPhi dst args)
            | None => None
          end
        | _ => None
      end
  end.