diff options
| -rw-r--r-- | backend/CSE3analysis.v | 12 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 20 | ||||
| -rw-r--r-- | lib/HashedSet.v | 14 |
3 files changed, 42 insertions, 4 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index bbe76f75..c88f06fa 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -128,14 +128,18 @@ Definition get_moves (eqs : PTree.t equation) : Record eq_context := mkeqcontext { eq_catalog : node -> option equation; - eq_kills : reg -> PSet.t; + eq_kill_reg : reg -> PSet.t; + eq_kill_mem : PSet.t; eq_moves : reg -> PSet.t }. Section OPERATIONS. Context {ctx : eq_context}. Definition kill_reg (r : reg) (rel : RELATION.t) : RELATION.t := - PSet.subtract rel (eq_kills ctx r). + PSet.subtract rel (eq_kill_reg ctx r). + + Definition kill_mem (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_mem ctx). Definition pick_source (l : list reg) := (* todo: take min? *) match l with @@ -159,7 +163,9 @@ Section OPERATIONS. | _ => x end end. - + + Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := + List.map (forward_move rel). End OPERATIONS. Definition totoro := RELATION.lub. diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index b14f3964..027a874a 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -277,6 +277,8 @@ Section SOUNDNESS. assumption. Qed. + Hint Resolve kill_reg_sound : cse3. + Lemma pick_source_sound : forall (l : list reg), match pick_source l with @@ -289,6 +291,8 @@ Section SOUNDNESS. left; trivial. Qed. + Hint Resolve pick_source_sound : cse3. + Theorem forward_move_sound : forall rel rs m x, (sem_rel rel rs m) -> @@ -323,6 +327,20 @@ Section SOUNDNESS. intuition congruence. Qed. + Hint Resolve forward_move_sound : cse3. + + Theorem forward_move_l_sound : + forall rel rs m l, + (sem_rel rel rs m) -> + rs ## (forward_move_l (ctx := ctx) rel l) = rs ## l. + Proof. + induction l; simpl; intros; trivial. + erewrite forward_move_sound by eassumption. + intuition congruence. + Qed. + + Hint Resolve forward_move_l_sound : cse3. + Theorem kill_mem_sound : forall rel rs m m', (sem_rel rel rs m) -> @@ -353,4 +371,6 @@ Section SOUNDNESS. intuition. congruence. Qed. + + Hint Resolve kill_mem_sound : cse3. End SOUNDNESS. diff --git a/lib/HashedSet.v b/lib/HashedSet.v index bd9cd9c0..00e01612 100644 --- a/lib/HashedSet.v +++ b/lib/HashedSet.v @@ -1058,6 +1058,10 @@ Axiom elements_complete: forall (m: t) (i: positive), In i (elements m) -> contains m i = true. +Axiom elements_spec: + forall (m: t) (i: positive), + In i (elements m) <-> contains m i = true. + Parameter fold: forall {B : Type}, (B -> positive -> B) -> t -> B -> B. @@ -1304,7 +1308,6 @@ Proof. apply PSet_internals.elements_correct. Qed. - Theorem elements_complete: forall (m: pset) (i: positive), In i (elements m) -> contains m i = true. @@ -1314,6 +1317,15 @@ Proof. Qed. +Theorem elements_spec: + forall (m: pset) (i: positive), + In i (elements m) <-> contains m i = true. +Proof. + intros. split. + - apply elements_complete. + - apply elements_correct. +Qed. + Definition fold {B : Type} (f : B -> positive -> B) (m : t) (v : B) : B := PSet_internals.fold f (pset_x m) v. |