Library CompOptCert.Syntax
Require Import RelationClasses.
Require Import List.
Require Import Maps.
Require Import Coqlib.
Require Import LibTactics.
Require Import Basics.
Require Import sflib.
Require Import Basic.
Require Import Loc.
Require Import Axioms.
Require Import Language.
Require Import Event.
Require Import Integers.
Set Implicit Arguments.
Require Import List.
Require Import Maps.
Require Import Coqlib.
Require Import LibTactics.
Require Import Basics.
Require Import sflib.
Require Import Basic.
Require Import Loc.
Require Import Axioms.
Require Import Language.
Require Import Event.
Require Import Integers.
Set Implicit Arguments.
Syntax of the CSimpRTL Language
Module Reg := Ident.
Module RegSet := IdentSet.
Module RegMap := IdentMap.
Module RegFun := IdentFun.
Module Op2.
Inductive t :=
| add
| sub
| mul
.
Definition eval (op:t): ∀ (op1 op2:int), int :=
match op with
| add ⇒ Int.add
| sub ⇒ Int.sub
| mul ⇒ Int.mul
end.
Definition eqb (op1 op2: t): bool :=
match op1, op2 with
| add, add ⇒ true
| sub, sub ⇒ true
| mul, mul ⇒ true
| _, _ ⇒ false
end.
Definition eq_dec : ∀ op1 op2: t, {op1 = op2} + {op1 ≠ op2}.
decide equality.
Defined.
End Op2.
Module Inst.
Inductive expr :=
| expr_val (val: int)
| expr_reg (reg: Reg.t)
| expr_op2 (op: Op2.t) (op1 op2: expr)
.
Definition expr_eq_dec: ∀ e1 e2: expr, {e1 = e2} + {e1 ≠ e2}.
decide equality. eapply Int.eq_dec. eapply Loc.eq_dec. eapply Op2.eq_dec.
Defined.
Definition beq_expr (e1 e2: expr): bool :=
expr_eq_dec e1 e2.
Lemma beq_expr_eq:
∀ e e',
beq_expr e e' = true ↔ e = e'.
Proof.
intros.
split.
- intro.
unfolds beq_expr.
unfolds Coqlib.proj_sumbool.
des_ifs.
- intro.
unfolds beq_expr.
unfolds Coqlib.proj_sumbool.
des_ifs.
Qed.
Fixpoint regs_of_expr (r:expr): RegSet.t :=
match r with
| expr_val val ⇒ RegSet.empty
| expr_reg reg ⇒ RegSet.singleton reg
| expr_op2 _ op1 op2 ⇒ RegSet.union (regs_of_expr op1) (regs_of_expr op2)
end.
Inductive expr :=
| expr_val (val: int)
| expr_reg (reg: Reg.t)
| expr_op2 (op: Op2.t) (op1 op2: expr)
.
Definition expr_eq_dec: ∀ e1 e2: expr, {e1 = e2} + {e1 ≠ e2}.
decide equality. eapply Int.eq_dec. eapply Loc.eq_dec. eapply Op2.eq_dec.
Defined.
Definition beq_expr (e1 e2: expr): bool :=
expr_eq_dec e1 e2.
Lemma beq_expr_eq:
∀ e e',
beq_expr e e' = true ↔ e = e'.
Proof.
intros.
split.
- intro.
unfolds beq_expr.
unfolds Coqlib.proj_sumbool.
des_ifs.
- intro.
unfolds beq_expr.
unfolds Coqlib.proj_sumbool.
des_ifs.
Qed.
Fixpoint regs_of_expr (r:expr): RegSet.t :=
match r with
| expr_val val ⇒ RegSet.empty
| expr_reg reg ⇒ RegSet.singleton reg
| expr_op2 _ op1 op2 ⇒ RegSet.union (regs_of_expr op1) (regs_of_expr op2)
end.
Instruction includes:
Inductive t :=
| skip
| assign (lhs: Reg.t) (rhs: expr)
| load (lhs: Reg.t) (loc: Loc.t) (or: Ordering.t)
| store (lhs: Loc.t) (rhs: expr) (ow: Ordering.t)
| print (e: expr)
| cas (lhs: Reg.t) (loc: Loc.t) (er ew: expr) (or ow: Ordering.t)
| fence_rel
| fence_acq
| fence_sc
.
Definition regs_of (i:t): RegSet.t :=
match i with
| skip ⇒ RegSet.empty
| assign reg rhs ⇒ RegSet.add reg (regs_of_expr rhs)
| load reg loc _ ⇒ regs_of_expr (expr_reg reg)
| store loc rhs _ ⇒ regs_of_expr rhs
| cas r loc er ew _ _ ⇒
RegSet.add r (RegSet.union (regs_of_expr er) (regs_of_expr ew))
| print e ⇒ regs_of_expr e
| _ ⇒ RegSet.empty
end.
End Inst.
| skip
| assign (lhs: Reg.t) (rhs: expr)
| load (lhs: Reg.t) (loc: Loc.t) (or: Ordering.t)
| store (lhs: Loc.t) (rhs: expr) (ow: Ordering.t)
| print (e: expr)
| cas (lhs: Reg.t) (loc: Loc.t) (er ew: expr) (or ow: Ordering.t)
| fence_rel
| fence_acq
| fence_sc
.
Definition regs_of (i:t): RegSet.t :=
match i with
| skip ⇒ RegSet.empty
| assign reg rhs ⇒ RegSet.add reg (regs_of_expr rhs)
| load reg loc _ ⇒ regs_of_expr (expr_reg reg)
| store loc rhs _ ⇒ regs_of_expr rhs
| cas r loc er ew _ _ ⇒
RegSet.add r (RegSet.union (regs_of_expr er) (regs_of_expr ew))
| print e ⇒ regs_of_expr e
| _ ⇒ RegSet.empty
end.
End Inst.
Basic Block
A list of instructions with a jmp (unconditional branch), or call (function call) or be (conditional branch) or ret (function return) instructions as a tail.
Module BBlock.
Inductive t :=
| jmp (f: Language.fid)
| call (f fret: Language.fid)
| be (e: Inst.expr) (f1 f2: Language.fid)
| ret
| blk (c: Inst.t) (b: t).
Fixpoint regs_of_blk (BB: t): RegSet.t :=
match BB with
| jmp f ⇒ RegSet.empty
| call f fret ⇒ RegSet.empty
| ret ⇒ RegSet.empty
| be e f1 f2 ⇒ Inst.regs_of_expr e
| blk c BB' ⇒ RegSet.union (Inst.regs_of c) (regs_of_blk BB')
end.
Fixpoint get_out_fids (bb: t): list(Language.fid) :=
match bb with
| blk _ bb' ⇒ get_out_fids bb'
| jmp fid ⇒ fid::nil
| call f fret ⇒ fret::nil
| be _ fid1 fid2 ⇒ fid1::(fid2::nil)
| _ ⇒ nil
end.
Fixpoint bb_from_i (bb: t) (i: nat) {struct i} : option t :=
match i with
| O ⇒ Some bb
| S i' ⇒
match bb with
| blk _ bb' ⇒ bb_from_i bb' i'
| _ ⇒ None
end
end.
Fixpoint len (bb: t) :=
match bb with
| blk c bb' ⇒ len(bb') + 1
| _ ⇒ 1
end.
Lemma len_lt_zero:
∀ bb,
len bb > 0.
Proof.
intros.
unfolds len.
destruct bb; try lia.
Qed.
Lemma len_lt:
∀ i bb bb',
bb_from_i bb i = Some bb' →
i < len bb.
Proof.
induction i.
intros.
pose proof (len_lt_zero bb). lia.
intros.
unfold bb_from_i in H.
destruct bb; try discriminate; eauto. folds bb_from_i .
eapply IHi in H.
unfold len. fold len.
lia.
Qed.
Lemma len_divide:
∀ i bb bb',
bb_from_i bb i = Some bb' →
i + len bb' = len bb.
Proof.
induction i.
intros.
unfold bb_from_i in H.
inv H. lia.
intros.
unfold bb_from_i in H.
destruct bb; try discriminate; eauto. folds bb_from_i .
eapply IHi in H.
unfold len. fold len.
lia.
Qed.
Lemma len_lt_one:
∀ bb,
(∃ i' bb',
bb = blk i' bb'
)
→
len bb > 1.
Proof.
intros.
destruct H as (inst' & bb' & BLK).
rewrite BLK.
unfold len; try discriminate. fold len.
pose proof (len_lt_zero bb'). lia.
Qed.
Lemma len_eq_one:
∀ bb,
(∀ i' bb',
bb ≠ blk i' bb'
)
→
len bb = 1.
Proof.
intros.
pose proof (classic (len bb = 1)).
destruct H0; trivial.
{
exfalso.
pose proof (len_lt_zero bb).
destruct bb; unfolds len; try lia.
folds len.
pose proof (H c bb). contradiction.
}
Qed.
Lemma len_eq:
∀ i bb bb',
bb_from_i bb i = Some bb' →
(∀ i' bb'',
bb' ≠ blk i' bb''
)
→
i+1 = len bb.
Proof.
induction i.
-
intros.
unfold bb_from_i in H.
inversion H. simpl.
eapply eq_sym.
eapply len_eq_one; eauto.
-
intros.
eapply len_divide in H.
eapply len_eq_one in H0; eauto.
rewrite H0 in H. trivial.
Qed.
Lemma len_none:
∀ i bb,
bb_from_i bb i = None ↔
i ≥ len bb.
Proof.
induction i.
-
intros.
split.
unfolds bb_from_i. discriminate.
intros.
pose proof (len_lt_zero bb).
lia.
-
intros.
split.
{
intros.
unfold bb_from_i in H.
folds bb_from_i.
destruct bb; unfolds len; try lia.
eapply IHi in H.
lia.
}
{
intros.
unfold len in H.
destruct bb;
unfolds bb_from_i; trivial.
folds bb_from_i.
folds len.
assert (i ≥ len bb). {
lia.
}
eapply IHi in H0.
trivial.
}
Qed.
Lemma len_none_plus:
∀ bb i i',
bb_from_i bb i = None →
i' ≥ i →
bb_from_i bb i' = None.
Proof.
intros.
eapply len_none in H.
assert (i' ≥ len bb). {lia. }
eapply len_none in H1.
trivial.
Qed.
End BBlock.
Notation "i ## b" := (BBlock.blk i b) (at level 69, right associativity).
Notation "b [ i :]" := (BBlock.bb_from_i b i) (at level 1, right associativity).
Inductive t :=
| jmp (f: Language.fid)
| call (f fret: Language.fid)
| be (e: Inst.expr) (f1 f2: Language.fid)
| ret
| blk (c: Inst.t) (b: t).
Fixpoint regs_of_blk (BB: t): RegSet.t :=
match BB with
| jmp f ⇒ RegSet.empty
| call f fret ⇒ RegSet.empty
| ret ⇒ RegSet.empty
| be e f1 f2 ⇒ Inst.regs_of_expr e
| blk c BB' ⇒ RegSet.union (Inst.regs_of c) (regs_of_blk BB')
end.
Fixpoint get_out_fids (bb: t): list(Language.fid) :=
match bb with
| blk _ bb' ⇒ get_out_fids bb'
| jmp fid ⇒ fid::nil
| call f fret ⇒ fret::nil
| be _ fid1 fid2 ⇒ fid1::(fid2::nil)
| _ ⇒ nil
end.
Fixpoint bb_from_i (bb: t) (i: nat) {struct i} : option t :=
match i with
| O ⇒ Some bb
| S i' ⇒
match bb with
| blk _ bb' ⇒ bb_from_i bb' i'
| _ ⇒ None
end
end.
Fixpoint len (bb: t) :=
match bb with
| blk c bb' ⇒ len(bb') + 1
| _ ⇒ 1
end.
Lemma len_lt_zero:
∀ bb,
len bb > 0.
Proof.
intros.
unfolds len.
destruct bb; try lia.
Qed.
Lemma len_lt:
∀ i bb bb',
bb_from_i bb i = Some bb' →
i < len bb.
Proof.
induction i.
intros.
pose proof (len_lt_zero bb). lia.
intros.
unfold bb_from_i in H.
destruct bb; try discriminate; eauto. folds bb_from_i .
eapply IHi in H.
unfold len. fold len.
lia.
Qed.
Lemma len_divide:
∀ i bb bb',
bb_from_i bb i = Some bb' →
i + len bb' = len bb.
Proof.
induction i.
intros.
unfold bb_from_i in H.
inv H. lia.
intros.
unfold bb_from_i in H.
destruct bb; try discriminate; eauto. folds bb_from_i .
eapply IHi in H.
unfold len. fold len.
lia.
Qed.
Lemma len_lt_one:
∀ bb,
(∃ i' bb',
bb = blk i' bb'
)
→
len bb > 1.
Proof.
intros.
destruct H as (inst' & bb' & BLK).
rewrite BLK.
unfold len; try discriminate. fold len.
pose proof (len_lt_zero bb'). lia.
Qed.
Lemma len_eq_one:
∀ bb,
(∀ i' bb',
bb ≠ blk i' bb'
)
→
len bb = 1.
Proof.
intros.
pose proof (classic (len bb = 1)).
destruct H0; trivial.
{
exfalso.
pose proof (len_lt_zero bb).
destruct bb; unfolds len; try lia.
folds len.
pose proof (H c bb). contradiction.
}
Qed.
Lemma len_eq:
∀ i bb bb',
bb_from_i bb i = Some bb' →
(∀ i' bb'',
bb' ≠ blk i' bb''
)
→
i+1 = len bb.
Proof.
induction i.
-
intros.
unfold bb_from_i in H.
inversion H. simpl.
eapply eq_sym.
eapply len_eq_one; eauto.
-
intros.
eapply len_divide in H.
eapply len_eq_one in H0; eauto.
rewrite H0 in H. trivial.
Qed.
Lemma len_none:
∀ i bb,
bb_from_i bb i = None ↔
i ≥ len bb.
Proof.
induction i.
-
intros.
split.
unfolds bb_from_i. discriminate.
intros.
pose proof (len_lt_zero bb).
lia.
-
intros.
split.
{
intros.
unfold bb_from_i in H.
folds bb_from_i.
destruct bb; unfolds len; try lia.
eapply IHi in H.
lia.
}
{
intros.
unfold len in H.
destruct bb;
unfolds bb_from_i; trivial.
folds bb_from_i.
folds len.
assert (i ≥ len bb). {
lia.
}
eapply IHi in H0.
trivial.
}
Qed.
Lemma len_none_plus:
∀ bb i i',
bb_from_i bb i = None →
i' ≥ i →
bb_from_i bb i' = None.
Proof.
intros.
eapply len_none in H.
assert (i' ≥ len bb). {lia. }
eapply len_none in H1.
trivial.
Qed.
End BBlock.
Notation "i ## b" := (BBlock.blk i b) (at level 69, right associativity).
Notation "b [ i :]" := (BBlock.bb_from_i b i) (at level 1, right associativity).
fid -> bblock
Function
A pair of codeheap and a label indicating the function entry. In our paper (in Figure 4), for simple presentation, we assume that the entry of each function equals to its function identifier.
Definition Code:Type := PTree.t Func.
Fixpoint regs_of_cdhp' (BS: list (positive × BBlock.t)) :=
match BS with
| nil ⇒ RegSet.empty
| (l, BB) :: BS' ⇒ RegSet.union (BBlock.regs_of_blk BB) (regs_of_cdhp' BS')
end.
Definition regs_of_cdhp (cdhp: CodeHeap) :=
regs_of_cdhp' (PTree.elements cdhp).
Definition succ (bb: BBlock.t): list(Language.fid) := BBlock.get_out_fids bb.
Inductive pred (cdhp: CodeHeap) (f: Language.fid): ∀ (f': Language.fid), Prop :=
| pred_intro
f' bb
(VALID: cdhp!f' = Some bb)
(PRED: In f (succ bb))
:
pred cdhp f f'
.
Theorem subblk_same_succ:
∀ blk inst blk',
blk = inst ## blk' →
succ blk = succ blk'.
Proof.
intros.
unfolds succ.
unfolds BBlock.get_out_fids. rewrite H. trivial.
Qed.
Definition bb_from_i := BBlock.bb_from_i.
Theorem bb_from_zero:
∀ blk,
blk[0:] = Some blk.
Proof.
intros.
unfolds BBlock.bb_from_i.
induction blk; trivial.
Qed.
Theorem bb_from_i_plus_one:
∀ i blk inst b',
blk [i:] = Some (inst ## b')
→
blk [i+1:] = Some (b').
Proof.
induction i.
-
intros.
unfolds BBlock.bb_from_i.
destruct blk; try inversion H; eauto.
-
intros.
simpls.
destruct blk; eauto; try discriminate.
Qed.
Theorem bb_from_i_gnone:
∀ i blk inst blk',
blk = inst ## blk'
→
blk [i:] = None
→
blk' [i:] = None
.
Proof.
induction i.
intros.
- unfolds BBlock.bb_from_i. discriminate.
- intros.
unfolds BBlock.bb_from_i. rewrite H in H0.
destruct blk' eqn:EqBlk'; trivial.
eapply BBlock.len_none in H0.
folds BBlock.bb_from_i.
eapply BBlock.len_none.
assert (∃ i', i = S i'). {
pose proof (BBlock.len_lt_zero (c ## t)).
destruct i; try lia.
∃ i. trivial.
}
destruct H1 as (i' & H1).
rewrite H1.
rewrite H1 in H0.
folds bb_from_i.
eapply BBlock.len_none.
eapply BBlock.len_none in H0.
rewrite <- EqBlk' in H0.
eapply IHi in EqBlk'; eauto.
eapply BBlock.len_none_plus with (i' := S i') in EqBlk'; eauto; try lia.
rewrite H1; trivial.
Qed.
Theorem bb_from_i_geq:
∀ i blk inst blk' blk'',
blk = inst ## blk'
→
blk' [i:] = blk''
→
blk [i+1:] = blk''
.
Proof.
induction i.
- intros.
unfolds BBlock.bb_from_i. simpls.
rewrite H. trivial.
- intros.
unfolds BBlock.bb_from_i. simpls.
rewrite H.
replace (i+1) with (S i); try lia.
trivial.
Qed.
Theorem bb_from_i_plus_one_implies_i:
∀ i blk blk'',
blk [S i:] = Some blk''
→
∃ inst,
blk [i:] = Some (inst##blk'').
Proof.
induction i.
-
intros.
unfolds BBlock.bb_from_i.
destruct blk eqn:EqBlk; try discriminate.
inv H.
∃ c. econs.
-
intros.
unfolds BBlock.bb_from_i.
destruct blk eqn:EqBlk; try discriminate.
folds BBlock.bb_from_i.
destruct t eqn:EqT; try discriminate; eauto.
Qed.
Theorem bb_from_i_invariant:
∀ i blk blk',
blk [i:] = Some blk'
→
BBlock.len blk = i + BBlock.len blk'.
Proof.
induction i.
-
intros.
unfolds BBlock.bb_from_i. inv H. lia.
-
intros.
eapply bb_from_i_plus_one_implies_i in H.
destruct H as (inst & H).
eapply IHi in H.
rewrite H.
unfold BBlock.len; simpls.
lia.
Qed.
Theorem blk_partial_i_lt_len:
∀ i blk blk',
blk[i:] = Some blk'
→
i < BBlock.len blk.
Proof.
intros.
eapply bb_from_i_invariant in H.
pose proof (BBlock.len_lt_zero blk').
rewrite H.
eapply Nat.lt_sub_lt_add_l.
lia.
Qed.
Lemma reg_in_blk_in_cdhp':
∀ m l BB r
(IN: In (l, BB) m)
(REG: RegSet.In r (BBlock.regs_of_blk BB)),
RegSet.In r (regs_of_cdhp' m).
Proof.
induction m; ii; ss; eauto.
destruct a. des1.
- inv IN. eapply RegSet.union_spec. eauto.
- eapply RegSet.union_spec; eauto.
Qed.
Theorem reg_in_blk_in_cdhp
r BB l cdhp
(REG_BLK: RegSet.In r (BBlock.regs_of_blk BB))
(GET: cdhp ! l = Some BB):
RegSet.In r (regs_of_cdhp cdhp).
Proof.
unfold regs_of_cdhp.
eapply reg_in_blk_in_cdhp'; eauto.
instantiate (1 := l).
eapply PTree.elements_correct; eauto.
Qed.
Fixpoint regs_of_cdhp' (BS: list (positive × BBlock.t)) :=
match BS with
| nil ⇒ RegSet.empty
| (l, BB) :: BS' ⇒ RegSet.union (BBlock.regs_of_blk BB) (regs_of_cdhp' BS')
end.
Definition regs_of_cdhp (cdhp: CodeHeap) :=
regs_of_cdhp' (PTree.elements cdhp).
Definition succ (bb: BBlock.t): list(Language.fid) := BBlock.get_out_fids bb.
Inductive pred (cdhp: CodeHeap) (f: Language.fid): ∀ (f': Language.fid), Prop :=
| pred_intro
f' bb
(VALID: cdhp!f' = Some bb)
(PRED: In f (succ bb))
:
pred cdhp f f'
.
Theorem subblk_same_succ:
∀ blk inst blk',
blk = inst ## blk' →
succ blk = succ blk'.
Proof.
intros.
unfolds succ.
unfolds BBlock.get_out_fids. rewrite H. trivial.
Qed.
Definition bb_from_i := BBlock.bb_from_i.
Theorem bb_from_zero:
∀ blk,
blk[0:] = Some blk.
Proof.
intros.
unfolds BBlock.bb_from_i.
induction blk; trivial.
Qed.
Theorem bb_from_i_plus_one:
∀ i blk inst b',
blk [i:] = Some (inst ## b')
→
blk [i+1:] = Some (b').
Proof.
induction i.
-
intros.
unfolds BBlock.bb_from_i.
destruct blk; try inversion H; eauto.
-
intros.
simpls.
destruct blk; eauto; try discriminate.
Qed.
Theorem bb_from_i_gnone:
∀ i blk inst blk',
blk = inst ## blk'
→
blk [i:] = None
→
blk' [i:] = None
.
Proof.
induction i.
intros.
- unfolds BBlock.bb_from_i. discriminate.
- intros.
unfolds BBlock.bb_from_i. rewrite H in H0.
destruct blk' eqn:EqBlk'; trivial.
eapply BBlock.len_none in H0.
folds BBlock.bb_from_i.
eapply BBlock.len_none.
assert (∃ i', i = S i'). {
pose proof (BBlock.len_lt_zero (c ## t)).
destruct i; try lia.
∃ i. trivial.
}
destruct H1 as (i' & H1).
rewrite H1.
rewrite H1 in H0.
folds bb_from_i.
eapply BBlock.len_none.
eapply BBlock.len_none in H0.
rewrite <- EqBlk' in H0.
eapply IHi in EqBlk'; eauto.
eapply BBlock.len_none_plus with (i' := S i') in EqBlk'; eauto; try lia.
rewrite H1; trivial.
Qed.
Theorem bb_from_i_geq:
∀ i blk inst blk' blk'',
blk = inst ## blk'
→
blk' [i:] = blk''
→
blk [i+1:] = blk''
.
Proof.
induction i.
- intros.
unfolds BBlock.bb_from_i. simpls.
rewrite H. trivial.
- intros.
unfolds BBlock.bb_from_i. simpls.
rewrite H.
replace (i+1) with (S i); try lia.
trivial.
Qed.
Theorem bb_from_i_plus_one_implies_i:
∀ i blk blk'',
blk [S i:] = Some blk''
→
∃ inst,
blk [i:] = Some (inst##blk'').
Proof.
induction i.
-
intros.
unfolds BBlock.bb_from_i.
destruct blk eqn:EqBlk; try discriminate.
inv H.
∃ c. econs.
-
intros.
unfolds BBlock.bb_from_i.
destruct blk eqn:EqBlk; try discriminate.
folds BBlock.bb_from_i.
destruct t eqn:EqT; try discriminate; eauto.
Qed.
Theorem bb_from_i_invariant:
∀ i blk blk',
blk [i:] = Some blk'
→
BBlock.len blk = i + BBlock.len blk'.
Proof.
induction i.
-
intros.
unfolds BBlock.bb_from_i. inv H. lia.
-
intros.
eapply bb_from_i_plus_one_implies_i in H.
destruct H as (inst & H).
eapply IHi in H.
rewrite H.
unfold BBlock.len; simpls.
lia.
Qed.
Theorem blk_partial_i_lt_len:
∀ i blk blk',
blk[i:] = Some blk'
→
i < BBlock.len blk.
Proof.
intros.
eapply bb_from_i_invariant in H.
pose proof (BBlock.len_lt_zero blk').
rewrite H.
eapply Nat.lt_sub_lt_add_l.
lia.
Qed.
Lemma reg_in_blk_in_cdhp':
∀ m l BB r
(IN: In (l, BB) m)
(REG: RegSet.In r (BBlock.regs_of_blk BB)),
RegSet.In r (regs_of_cdhp' m).
Proof.
induction m; ii; ss; eauto.
destruct a. des1.
- inv IN. eapply RegSet.union_spec. eauto.
- eapply RegSet.union_spec; eauto.
Qed.
Theorem reg_in_blk_in_cdhp
r BB l cdhp
(REG_BLK: RegSet.In r (BBlock.regs_of_blk BB))
(GET: cdhp ! l = Some BB):
RegSet.In r (regs_of_cdhp cdhp).
Proof.
unfold regs_of_cdhp.
eapply reg_in_blk_in_cdhp'; eauto.
instantiate (1 := l).
eapply PTree.elements_correct; eauto.
Qed.