diff options
-rw-r--r-- | backend/CSE2.v | 48 | ||||
-rw-r--r-- | backend/CSE2proof.v | 103 |
2 files changed, 95 insertions, 56 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index 5b850cbb..07bde1ac 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -275,24 +275,6 @@ Definition forward_move (rel : RELATION.t) (x : reg) : reg := Definition move (src dst : reg) (rel : RELATION.t) := PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel). -Definition oper1 (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) := - let rel' := kill_reg dst rel in - PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'. - -Definition oper (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) := - if List.in_dec peq dst args - then kill_reg dst rel - else oper1 op dst args rel. - -Definition gen_oper (op: operation) (dst : reg) (args : list reg) - (rel : RELATION.t) := - match op, args with - | Omove, src::nil => move src dst rel - | _, _ => oper op dst args rel - end. - Definition find_op_fold op args (already : option reg) x sv := match already with | Some found => already @@ -309,6 +291,31 @@ Definition find_op_fold op args (already : option reg) x sv := Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) := PTree.fold (find_op_fold op args) rel None. +Definition oper2 (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + let rel' := kill_reg dst rel in + PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'. + +Definition oper1 (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + if List.in_dec peq dst args + then kill_reg dst rel + else oper2 op dst args rel. + +Definition oper (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + match find_op rel op args with + | Some r => move r dst rel + | None => oper1 op dst args rel + end. + +Definition gen_oper (op: operation) (dst : reg) (args : list reg) + (rel : RELATION.t) := + match op, args with + | Omove, src::nil => move src dst rel + | _, _ => oper op dst args rel + end. + (* NO LONGER NEEDED Fixpoint list_represents { X : Type } (l : list (positive*X)) (tr : PTree.t X) : Prop := match l with @@ -392,8 +399,9 @@ Definition transf_instr (fmap : option (PMap.t RB.t)) (pc: node) (instr: instruction) := match instr with | Iop op args dst s => - match find_op_in_fmap fmap pc op args with - | None => Iop op (subst_args fmap pc args) dst s + let args' := subst_args fmap pc args in + match find_op_in_fmap fmap pc op args' with + | None => Iop op args' dst s | Some src => Iop Omove (src::nil) dst s end | Iload chunk addr args dst s => diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 1d0a617a..47b60902 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -249,7 +249,7 @@ Proof. destruct s; simpl in *; destruct negb; simpl; congruence. Qed. -Lemma oper1_sound : +Lemma oper2_sound : forall rel : RELATION.t, forall op : operation, forall dst : reg, @@ -259,12 +259,12 @@ Lemma oper1_sound : sem_rel rel rs -> not (In dst args) -> eval_operation genv sp op (rs ## args) m = Some v -> - sem_rel (oper1 op dst args rel) (rs # dst <- v). + sem_rel (oper2 op dst args rel) (rs # dst <- v). Proof. intros until v. intros REL NOT_IN EVAL x. pose proof (kill_reg_sound rel dst rs v REL x) as KILL. - unfold oper1. + unfold oper2. destruct (peq x dst). { subst x. @@ -282,7 +282,7 @@ Proof. exact KILL. Qed. -Lemma oper_sound : +Lemma oper1_sound : forall rel : RELATION.t, forall op : operation, forall dst : reg, @@ -291,45 +291,18 @@ Lemma oper_sound : forall v, sem_rel rel rs -> eval_operation genv sp op (rs ## args) m = Some v -> - sem_rel (oper op dst args rel) (rs # dst <- v). + sem_rel (oper1 op dst args rel) (rs # dst <- v). Proof. intros until v. intros REL EVAL. - unfold oper. + unfold oper1. destruct in_dec. { apply kill_reg_sound; auto. } - apply oper1_sound; auto. + apply oper2_sound; auto. Qed. -Lemma gen_oper_sound : - forall rel : RELATION.t, - forall op : operation, - forall dst : reg, - forall args: list reg, - forall rs : regset, - forall v, - sem_rel rel rs -> - eval_operation genv sp op (rs ## args) m = Some v -> - sem_rel (gen_oper op dst args rel) (rs # dst <- v). -Proof. - intros until v. - intros REL EVAL. - unfold gen_oper. - destruct op. - { destruct args as [ | h0 t0]. - apply oper_sound; auto. - destruct t0. - { - simpl in *. - replace v with (rs # h0) by congruence. - apply move_sound; auto. - } - apply oper_sound; auto. - } - all: apply oper_sound; auto. -Qed. Lemma find_op_sound : @@ -399,6 +372,59 @@ Proof. apply REC; auto. Qed. +Lemma oper_sound : + forall rel : RELATION.t, + forall op : operation, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall v, + sem_rel rel rs -> + eval_operation genv sp op (rs ## args) m = Some v -> + sem_rel (oper op dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL EVAL. + unfold oper. + destruct find_op eqn:FIND. + { + assert (eval_operation genv sp op rs ## args m = Some rs # r). + { + apply (find_op_sound rel); trivial. + } + replace v with (rs # r) by congruence. + apply move_sound; auto. + } + apply oper1_sound; trivial. +Qed. + +Lemma gen_oper_sound : + forall rel : RELATION.t, + forall op : operation, + forall dst : reg, + forall args: list reg, + forall rs : regset, + forall v, + sem_rel rel rs -> + eval_operation genv sp op (rs ## args) m = Some v -> + sem_rel (gen_oper op dst args rel) (rs # dst <- v). +Proof. + intros until v. + intros REL EVAL. + unfold gen_oper. + destruct op. + { destruct args as [ | h0 t0]. + apply oper_sound; auto. + destruct t0. + { + simpl in *. + replace v with (rs # h0) by congruence. + apply move_sound; auto. + } + apply oper_sound; auto. + } + all: apply oper_sound; auto. +Qed. Lemma kill_reg_weaken: forall res mpc rs, @@ -645,8 +671,13 @@ Proof. { eapply exec_Iop with (v := v); eauto. simpl. - rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption. - assumption. + rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. + { + rewrite MAP in H0. + rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption. + assumption. + } + unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. } constructor; eauto. unfold fmap_sem', fmap_sem in *. |