Require Import Coq.Unicode.Utf8.
Require Recdef.
Require Import FSets.
Require Import Coqlib.
Require Import Ordered.
Require Import Errors.
Require Import Maps.
Require Import Lattice.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Globalenvs.
Require Import Events.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import RTLdfs.
Require Import Kildall.
Require Import KildallComp.
Require Import Conventions.
Require Import SSA.
Require Import SSAutils.
Require Import SSAvalid.
Require Import Utils.
Require Import Classical.
Require Import Bijection.

Unset Allow StrictProp.

Tactics

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
      | [ H1: ?Δ ! ?pc = _ ,
        H2: ?Δ ! ?pc = _ |- _ ] =>
      rewrite H1 in H2; inv H2
      | [ H: ?Γ _ = ?Γ _ |- _ ] => rewrite H in *
      | _ => idtac
    end.

Ltac elimAndb :=
  match goal with
  | [ H: _ && _ = true |- _ ] =>
      elim (andb_prop _ _ H); clear H; intros; elimAndb
  | _ =>
      idtac
  end.

The erasure function

Definition erase_reg (size: nat) (r: reg) := fst (Bij.rmap size r).
Definition get_index (size: nat) (r: reg) := snd (Bij.rmap size r).

Definition erase_instr (size: nat) instr : RTL.instruction :=
  match instr with
    | Inop n => RTL.Inop n
    | Iop op args dst succ =>
      RTL.Iop op (List.map (erase_reg size) args) (erase_reg size dst) succ
    | Iload chunk addr args dst succ =>
      RTL.Iload chunk addr (List.map (erase_reg size) args) (erase_reg size dst) succ
    | Istore chunk addr args src succ =>
      RTL.Istore chunk addr (List.map (erase_reg size) args) (erase_reg size src) succ
    | Icall sig fn args dst succ =>
      match fn with
        | inl r => RTL.Icall sig (inl ident (erase_reg size r)) (List.map (erase_reg size) args) (erase_reg size dst) succ
        | inr id => RTL.Icall sig (inr _ id) (List.map (erase_reg size) args) (erase_reg size dst) succ
      end
    | Itailcall sig fn args =>
      match fn with
        | inl r => RTL.Itailcall sig (inl ident (erase_reg size r)) (List.map (erase_reg size) args)
        | inr id => RTL.Itailcall sig (inr _ id) (List.map (erase_reg size) args)
      end
    | Ibuiltin fn args dst succ =>
      RTL.Ibuiltin fn
                   (List.map (map_builtin_arg (erase_reg size)) args)
                   (map_builtin_res (erase_reg size) dst)
                   succ
    | Icond cond args ifso ifnot =>
      RTL.Icond cond (List.map (erase_reg size) args) ifso ifnot
    | Ijumptable arg tbl =>
      RTL.Ijumptable (erase_reg size arg) tbl
    | Ireturn reg =>
      match reg with
        | None => RTL.Ireturn None
        | Some r => RTL.Ireturn (Some (erase_reg size r))
      end
  end.

Definition erase_code (size: nat) (rtlphi:function) : RTL.code :=
  PTree.map (fun pc i => erase_instr size i) (fn_code rtlphi).

Variant check_erased_spec (size: nat) (rtl: RTLdfs.function) (rtlphi:SSA.function) :=
| ces_intros: forall
  (HSIG : (RTLdfs.fn_sig rtl) = (SSA.fn_sig rtlphi))
  (HPARAMS: (RTLdfs.fn_params rtl) = (map (erase_reg size) (SSA.fn_params rtlphi)))
  (HSSIZE : (RTLdfs.fn_stacksize rtl) = (SSA.fn_stacksize rtlphi))
  (HENTRY : (RTLdfs.fn_entrypoint rtl) = (SSA.fn_entrypoint rtlphi))
  (HCODE: forall p, (RTLdfs.fn_code rtl) ! p = (erase_code size rtlphi) ! p),
  check_erased_spec size rtl rtlphi.
   
Lemma extensional_assigned_code_spec : forall m m' pc r,
  m ! pc = m' ! pc ->
  assigned_code_spec m pc r ->
  assigned_code_spec m' pc r.

Inductive check_args_spec (size: nat) : list Registers.reg -> list reg -> Prop :=
| check_args_nil: check_args_spec size nil nil
| check_args_cons:
  forall argl argl' arg,
    check_args_spec size argl argl' ->
    check_args_spec size ((erase_reg size arg)::argl) (arg::argl').

Lemma check_args_spec_erased_rwt: forall size args args',
  check_args_spec size args args' ->
  (List.map (erase_reg size) args') = args.

Lemma check_args_spec_erased: forall size args,
  check_args_spec size (List.map (erase_reg size) args) args.

Lemma check_args_spec_erased_rwt_iff : forall size args args',
    (List.map (erase_reg size) args') = args <->
    check_args_spec size args args'.

Inductive check_ros_spec (size: nat) : Registers.reg + ident -> reg + ident -> Prop :=
  | check_ros_reg: forall r,
    check_ros_spec size (inl ident (erase_reg size r)) (inl ident r)
  | check_ros_ident: forall id,
    check_ros_spec size (inr _ id) (inr reg id).

Variant check_instrs_spec (size: nat) (rtlphi:function) : RTL.instruction -> instruction -> Prop :=
| MInop: forall n,
  check_instrs_spec size rtlphi (RTL.Inop n) (Inop n)
| MIop: forall op args args' dst succ,
  (check_args_spec size args args') ->
  check_instrs_spec size rtlphi (RTL.Iop op args (erase_reg size dst) succ)
  (Iop op args' dst succ)
| MIload: forall chunk addr args args' dst succ,
  (check_args_spec size args args' ) ->
  check_instrs_spec size rtlphi (RTL.Iload chunk addr args (erase_reg size dst) succ)
  (Iload chunk addr args' dst succ)
| MIstore: forall chunk addr args args' src succ,
  (check_args_spec size args args' ) ->
  check_instrs_spec size rtlphi (RTL.Istore chunk addr args (erase_reg size src) succ)
  (Istore chunk addr args' src succ)
| MIcall: forall sig fn fn' args args' dst succ,
  (check_args_spec size args args' ) ->
  (check_ros_spec size fn fn') ->
  check_instrs_spec size rtlphi (RTL.Icall sig fn args (erase_reg size dst) succ)
   (Icall sig fn' args' dst succ)
| MItailcall: forall sig fn fn' args args',
  (check_args_spec size args args' ) ->
  (check_ros_spec size fn fn') ->
  check_instrs_spec size rtlphi (RTL.Itailcall sig fn args) (Itailcall sig fn' args')
| MIbuiltin: forall fn args args' dst succ,
  (check_args_spec size (params_of_builtin_args args) (params_of_builtin_args args') ) ->
  check_instrs_spec size rtlphi
                     (RTL.Ibuiltin fn args (map_builtin_res (erase_reg size) dst) succ)
                     (Ibuiltin fn args' dst succ)
| MIcond: forall cond args args' ifso ifnot,
  (check_args_spec size args args' ) ->
  check_instrs_spec size rtlphi (RTL.Icond cond args ifso ifnot)
  (Icond cond args' ifso ifnot)
| MIjumptable: forall arg tbl,
  check_instrs_spec size rtlphi (RTL.Ijumptable (erase_reg size arg) tbl) (Ijumptable arg tbl)
| MIreturn_none: check_instrs_spec size rtlphi (RTL.Ireturn None) (Ireturn None)
| MIreturn_some: forall r,
  check_instrs_spec size rtlphi (RTL.Ireturn (Some (erase_reg size r))) (Ireturn (Some r)).

Lemma check_instr_spec_erase: forall size f tf pc rinstr rinstr',
  check_erased_spec size f tf ->
  (RTLdfs.fn_code f)!pc = Some rinstr ->
  (fn_code tf)!pc = Some rinstr' ->
  (erase_instr size rinstr' = rinstr) /\ check_instrs_spec size tf rinstr rinstr'.
    
Set Printing Notations.

Lemma erase_funct_no_add: forall size tf f pc rinstr,
  check_erased_spec size f tf ->
  ((RTLdfs.fn_code f)!pc = Some rinstr) ->
  exists pinstr, (fn_code tf)!pc = Some pinstr.

Lemma erased_funct_erased_instr: forall size pc f tf rinstr,
  check_erased_spec size f tf ->
  (RTLdfs.fn_code f)!pc = Some rinstr ->
  exists pinstr,
    (SSA.fn_code tf) ! pc = Some pinstr
    /\ (rinstr = erase_instr size pinstr).

Definition assigned (ri: reg) (block:phiblock) :=
  exists args, In (Iphi args ri) block.

Definition erased_reg_assigned (size: nat) (r:Registers.reg) (block:phiblock) :=
  (exists ri, ((assigned ri block) /\ erase_reg size ri = r)).

Lemma not_erased_reg_assigned_cons: forall size r a block,
  ~ (erased_reg_assigned size r (a::block)) ->
  ~ (erased_reg_assigned size r block).

Lemma not_erased_reg_assigned_not_in: forall size r block,
  ~ erased_reg_assigned size r block ->
  forall x args, (erase_reg size x = r -> not (In (Iphi args x) block)).
 
Lemma erased_reg_assigned_dec: forall size r block,
  erased_reg_assigned size r block \/ not (erased_reg_assigned size r block).

Additional structural invariants

Definition check_phi_params_spec (rtlphi: function) :=
  forall pc pc0 phiinstr args dst k,
    rtlphi.(fn_phicode)!pc = Some phiinstr ->
    index_pred (make_predecessors (fn_code rtlphi) successors_instr) pc0 pc = Some k ->
    In (Iphi args dst) phiinstr ->
    (nth_okp k args).

Definition check_no_duplicates_spec (size: nat) (rtlphi:function) :=
  forall pc phiinstr args args' dst dst',
    rtlphi.(fn_phicode)!pc = Some phiinstr ->
    NoDup phiinstr ->
    In (Iphi args dst) phiinstr ->
    In (Iphi args' dst') phiinstr ->
    (args <> args' \/ dst <> dst') ->
    (erase_reg size dst) <> (erase_reg size dst').

Definition structural_checks_spec (size: nat) (rtl: RTLdfs.function) (rtlphi: SSA.function) :=
  (RTLdfs.fn_sig rtl = SSA.fn_sig rtlphi)
  /\ ((RTLdfs.fn_stacksize rtl) = (SSA.fn_stacksize rtlphi))
  /\ (check_erased_spec size rtl rtlphi)
  /\ (unique_def_spec rtlphi)
  /\ (check_phi_params_spec rtlphi)
  /\ (check_no_duplicates_spec size rtlphi).

Utility lemmas about junction points

Lemma is_joinpoint_iff_join_point_ssa : forall f jp,
  join_point jp f <-> is_joinpoint (make_predecessors (fn_code f) SSA.successors_instr) jp = true.

Lemma is_joinpoint_iff_join_point : forall f jp,
  RTLutils.join_point jp f <->
  is_joinpoint (make_predecessors (RTLdfs.fn_code f) RTLdfs.successors_instr) jp = true.

Utility lemmas for the checker check_unique_def

Lemma not_assigned_monotone : forall m r k i,
  m ! k = None ->
  (forall pc : node, ~ assigned_code_spec (PTree.set k i m) pc r) ->
  forall pc : node, ~ assigned_code_spec m pc r.

Lemma record_assigned_reg_phi_preserve : forall pc pc' phib t l r,
  t ! r = Some l ->
  In pc l ->
  exists l', (record_assigned_reg_phi t pc' phib) ! r = Some l' /\ In pc l'.

Lemma assigned_code_preserved : forall k i m pc r,
pc <> k ->
assigned_code_spec (PTree.set k i m) pc r ->
assigned_code_spec m pc r.

Global Hint Resolve assigned_code_preserved: core.

Lemma fold_record_preserve: forall t l pc r,
    t ! r = Some l ->
    In pc l ->
    forall code, exists l', (PTree.fold record_assigned_reg_phi code t) ! r = Some l' /\ In pc l'.
 
Lemma record_assigned_reg_phi_in_block : forall phib x r a k l,
  In (Iphi x r) phib ->
  (record_assigned_reg_phi a k phib) ! r = Some l
  -> In k l.

Lemma record_assigned_reg_phi_preserve2 : forall pc phib t l r,
  t ! r = Some l ->
  exists l', (record_assigned_reg_phi t pc phib) ! r = Some l'.
  
Lemma record_assigned_reg_phi_in_block2 : forall phib x r a k,
  In (Iphi x r) phib ->
  exists l, (record_assigned_reg_phi a k phib) ! r = Some l.

Lemma assigned_phi_spec_inlist2 : forall t code r pc,
  (assigned_phi_spec code pc r) ->
  exists l, ((PTree.fold record_assigned_reg_phi code t) ! r = Some l /\ In pc l).

Lemma record_assigned_reg_phi_inlist3_stronger : forall r pc phiinstr l m,
  m ! r = Some l ->
  NoDup phiinstr ->
  (forall x, In (Iphi x r) phiinstr ->
    (forall x', In (Iphi x' r) phiinstr -> x' = x) ->
    exists l', (record_assigned_reg_phi m pc phiinstr) ! r = Some (pc::l'++l))
  /\
  (forall x, In (Iphi x r) phiinstr ->
    (exists x', In (Iphi x' r) phiinstr /\ x' <> x) ->
    exists l', exists l'', (record_assigned_reg_phi m pc phiinstr) ! r = Some (pc::l'++pc::l''++l))
  /\
  ((forall x, ~ In (Iphi x r) phiinstr) ->
    (record_assigned_reg_phi m pc phiinstr) ! r = Some l)
.


Lemma record_assigned_reg_phi_inlist3_none_stronger : forall r pc phiinstr m,
  m ! r = None ->
  NoDup phiinstr ->
  (forall x, In (Iphi x r) phiinstr ->
    (forall x', In (Iphi x' r) phiinstr -> x' = x) ->
    exists l', (record_assigned_reg_phi m pc phiinstr) ! r = Some (pc::l'))
  /\
  (forall x, In (Iphi x r) phiinstr ->
    (exists x', In (Iphi x' r) phiinstr /\ x' <> x) ->
    exists l', exists l'', (record_assigned_reg_phi m pc phiinstr) ! r = Some (pc::l'++pc::l''))
  /\
  ((forall x, ~ In (Iphi x r) phiinstr) ->
    (record_assigned_reg_phi m pc phiinstr) ! r = None)
.

Lemma record_assigned_reg_phi_inlist2_stronger : forall r pc phiinstr l m,
  m ! r = Some l ->
  (forall x, In (Iphi x r) phiinstr ->
    exists l', (record_assigned_reg_phi m pc phiinstr) ! r = Some (pc::l'++l))
  /\
  ((forall x, ~ In (Iphi x r) phiinstr) ->
    (record_assigned_reg_phi m pc phiinstr) ! r = Some l)
.

Variant assigned_phi_spec_twice (phicode: phicode) (pc: node): reg -> Prop :=
  APhi2: forall phi dst,
    (phicode!pc) = Some phi ->
    (∃args : list reg, exists args',
      In (Iphi args dst) phi /\ In (Iphi args' dst) phi /\ args' <> args) ->
    assigned_phi_spec_twice phicode pc dst.

Lemma record_assigned_reg_phi_preserve3 : forall phiinstr a r pc l,
  a ! r = Some l ->
  exists l', (record_assigned_reg_phi a pc phiinstr) ! r = Some (l' ++ l).


Variant assigned_phi_spec_once (phicode: phicode) (pc: node): reg -> Prop :=
  APhi1: forall phi dst,
    (phicode!pc) = Some phi ->
    (∃args : list reg, In (Iphi args dst) phi /\
      forall args', In (Iphi args' dst) phi -> args' = args) ->
    (NoDup phi) ->
    assigned_phi_spec_once phicode pc dst.

Lemma assigned_phi_spec_none_stronger : forall r code t,
  t ! r = None ->
  (forall pc phi, code ! pc = Some phi -> NoDup phi) ->
  (forall pc phi, code ! pc = Some phi -> NoDup phi) ->
  (forall pc, (assigned_phi_spec_once code pc r) ->
    exists l',
      exists l'', (PTree.fold record_assigned_reg_phi code t) ! r = Some (l'++pc::l''))
  /\
  (forall pc, (assigned_phi_spec_twice code pc r) ->
    exists l',
      exists l'',
        exists l''', (PTree.fold record_assigned_reg_phi code t) ! r = Some (l'++pc::l''++pc::l'''))
  /\
  ((forall pc, ~ (assigned_phi_spec code pc r)) ->
      (PTree.fold record_assigned_reg_phi code t) ! r = None).

 
Lemma assigned_phi_spec_inlist2_stronger : forall r l code t,
  t ! r = Some l ->
  (forall pc, (assigned_phi_spec code pc r) ->
    exists l',
      exists l'', (PTree.fold record_assigned_reg_phi code t) ! r = Some (l'++pc::l''++l))
  /\
  ((forall pc, ~ (assigned_phi_spec code pc r)) ->
      (PTree.fold record_assigned_reg_phi code t) ! r = Some l).


Lemma ex_nodup {A: Type} :
  (forall x y:A, {x = y}+{x <> y}) ->
  forall (l: list A), NoDup l \/ ~ NoDup l.
  
Lemma assigned_code_spec_inlist2 : forall code r pc,
  (assigned_code_spec code pc r) ->
  exists l, ((PTree.fold record_assigned_reg code (PTree.empty (list positive))) ! r = Some l
    /\ In pc l).

Lemma check_unique_def_correct1 : forall tf,
  check_unique_def tf = true ->
  (forall (r : reg) (pc pc' : node),
    assigned_code_spec (fn_code tf) pc r ->
    assigned_code_spec (fn_code tf) pc' r -> pc = pc').

Lemma check_unique_def_correct2 : forall tf,
  check_unique_def tf = true ->
    (forall (r : reg) (pc pc' : node),
      assigned_phi_spec (fn_phicode tf) pc r ->
      assigned_phi_spec (fn_phicode tf) pc' r -> pc = pc').

     
Lemma check_unique_def_correct3_help : forall tf,
  check_unique_def tf = true ->
  (forall (r : reg) (pc pc' : node),
    assigned_code_spec (fn_code tf) pc r -> assigned_phi_spec (fn_phicode tf) pc' r -> False).

Lemma check_unique_def_correct31 : forall tf,
  check_unique_def tf = true ->
  (forall (r : reg) (pc pc' : node),
    (assigned_phi_spec (fn_phicode tf) pc' r) -> ~ assigned_code_spec (fn_code tf) pc r).

Lemma check_unique_def_correct32 : forall tf,
  check_unique_def tf = true ->
  (forall (r : reg) (pc pc' : node),
    (assigned_code_spec (fn_code tf) pc' r) -> ~ assigned_phi_spec (fn_phicode tf) pc r).

Lemma not_assigned_code_spec_none : forall code r,
  (forall pc, ~ assigned_code_spec code pc r) ->
  (PTree.fold record_assigned_reg code (PTree.empty (list positive))) ! r = None.

Lemma check_unique_def_correct41 : forall tf,
  check_unique_def tf = true ->
  (forall pc phi, tf.(fn_phicode) ! pc = Some phi -> NoDup phi) ->
  forall pc phiinstr, tf.(fn_phicode) ! pc = Some phiinstr ->
    (forall r args args',
      In (Iphi args r) phiinstr -> In (Iphi args' r) phiinstr -> args = args').

Inductive dup : list phiinstruction -> reg -> Prop :=
| dup_intro1: forall args reg phi,
    In (Iphi args reg) phi -> dup ((Iphi args reg)::phi) reg
| dup_intro2: forall r phi iphi,
   dup phi r -> dup (iphi::phi) r.

Lemma not_nodup_dup : forall phiblock,
  ~ NoDup phiblock ->
  exists r, dup phiblock r.

Lemma dup_v_in_v : forall phi v,
  dup phi v ->
  exists args, In (Iphi args v) phi.

Lemma dup_record_assigned_reg_phi : forall phi dst a pc,
  dup phi dst ->
  ∃l : list positive,
  (record_assigned_reg_phi a pc phi) ! dst = Some l ∧ List.length l ≥ 2.
  
Lemma dup_more_than_two : forall phicode t pc dst phi ,
  phicode ! pc = Some phi ->
  dup phi dst ->
  exists l,
    (PTree.fold record_assigned_reg_phi phicode t) ! dst = Some l
    /\ (List.length l >= 2)%nat.
   
Lemma check_unique_def_correct42 : forall tf,
  check_unique_def tf = true ->
  (forall pc phi, tf.(fn_phicode) ! pc = Some phi -> NoDup phi).

Lemma check_unique_def_correct : forall tf,
  check_unique_def tf = true ->
  unique_def_spec tf.
        
Lemma phi_store_copy: forall k block rs dst arg args
  (NODUP: NoDup block)
  (NODUP': (forall r args args',
    In (Iphi args r) block -> In (Iphi args' r) block → args = args'))
  (IN: In (Iphi args dst) block /\ nth_error args k = Some arg),
  (phi_store k block rs)# dst = rs# arg.

Lemma check_udef_spec_no_dup: forall tf pc block,
  unique_def_spec tf ->
   (fn_phicode tf) ! pc = Some block ->
   NoDup block.

Lemma phi_store_copy2: forall f,
  wf_ssa_function f ->
  forall rs pc phiinstr args arg dst k,
    (fn_phicode f) ! pc = Some phiinstr ->
    In (Iphi args dst) phiinstr ->
    nth_error args k = Some arg ->
    (phi_store k phiinstr rs) # dst = rs # arg.

Lemma phi_store_notin_preserved_map: forall k block rs args,
  (forall dst, In dst args -> forall phiargs, ~ In (Iphi phiargs dst) block)->
  (phi_store k block rs) ## args = rs ## args.