diff options
| -rw-r--r-- | backend/CSE3.v | 2 | ||||
| -rw-r--r-- | backend/CSE3analysis.v | 80 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 166 | ||||
| -rw-r--r-- | backend/CSE3proof.v | 7 |
4 files changed, 39 insertions, 216 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v index 58e179e2..df1c2bfc 100644 --- a/backend/CSE3.v +++ b/backend/CSE3.v @@ -58,7 +58,7 @@ Definition transf_instr (fmap : PMap.t RB.t) match instr with | Iop op args dst s => let args' := subst_args fmap pc args in - match (if andb (negb (Compopts.optim_CSE3_trivial_ops tt)) (is_trivial_op op) then None else find_op_in_fmap fmap pc op args') with + match (if is_trivial_op op then None else find_op_in_fmap fmap pc op args') with | None => Iop op args' dst s | Some src => Iop Omove (src::nil) dst s end diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index dbf1afe2..7316c9a9 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -227,22 +227,13 @@ Section OPERATIONS. Definition kill_mem (rel : RELATION.t) : RELATION.t := PSet.subtract rel (eq_kill_mem ctx tt). - Definition reg_min (x y : reg) := - if plt x y then x else y. - - Fixpoint reg_min_rec (l : list reg) (before : reg) := - match l with - | h::t => reg_min_rec t (reg_min before h) - | nil => before - end. - Definition pick_source (l : list reg) := (* todo: take min? *) match l with | h::t => Some h | nil => None end. - Definition forward_move1 (rel : RELATION.t) (x : reg) : reg := + Definition forward_move (rel : RELATION.t) (x : reg) : reg := match pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x))) with | None => x | Some eqno => @@ -259,37 +250,6 @@ Section OPERATIONS. end end. - Definition pick_min_source (l : list reg) := - match l with - | h::t => Some (reg_min_rec t h) - | nil => None - end. - - Fixpoint get_sources (x : reg) eqs := - match eqs with - | nil => nil - | eqno::others => - match eq_catalog ctx eqno with - | Some eq => - if is_smove (eq_op eq) && peq x (eq_lhs eq) - then - match eq_args eq with - | src::nil => src :: (get_sources x others) - | _ => get_sources x others - end - else get_sources x others - | _ => get_sources x others - end - end. - - Definition forward_move2 (rel : RELATION.t) (x : reg) : reg := - match pick_min_source (get_sources x (PSet.elements (PSet.inter rel (eq_moves ctx x)))) with - | None => x - | Some src => src - end. - - Definition forward_move := forward_move1. - Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := List.map (forward_move rel). @@ -322,14 +282,12 @@ Section OPERATIONS. Definition oper2 (dst : reg) (op: sym_op)(args : list reg) (rel : RELATION.t) : RELATION.t := + let rel' := kill_reg dst rel in match eq_find {| eq_lhs := dst; eq_op := op; eq_args:= args |} with - | Some id => - if PSet.contains rel id - then rel - else PSet.add id (kill_reg dst rel) - | None => kill_reg dst rel + | Some id => PSet.add id rel' + | None => rel' end. Definition oper1 (dst : reg) (op: sym_op) (args : list reg) @@ -349,6 +307,12 @@ Section OPERATIONS. | Some eq_id => PSet.add eq_id (kill_reg dst rel) | None => kill_reg dst rel end. + + Definition is_trivial_sym_op sop := + match sop with + | SOp op => is_trivial_op op + | SLoad _ _ => false + end. Definition oper (dst : reg) (op: sym_op) (args : list reg) (rel : RELATION.t) : RELATION.t := @@ -360,18 +324,18 @@ Section OPERATIONS. | _ => kill_reg dst rel end else - let args' := forward_move_l rel args in - match rhs_find op args' rel with - | Some r => - if Compopts.optim_CSE3_glb tt - then RELATION.glb (move r dst rel) - (RELATION.glb (oper1 dst op args' rel) - (oper1 dst op args rel)) - else RELATION.glb (oper1 dst op args' rel) - (oper1 dst op args rel) - | None => RELATION.glb (oper1 dst op args' rel) - (oper1 dst op args rel) - end. + if is_trivial_sym_op op + then kill_reg dst rel + else + let args' := forward_move_l rel args in + match rhs_find op args' rel with + | Some r => + if Compopts.optim_CSE3_glb tt + then RELATION.glb (move r dst rel) + (oper1 dst op args' rel) + else oper1 dst op args' rel + | None => oper1 dst op args' rel + end. Definition clever_kill_store (chunk : memory_chunk) (addr: addressing) (args : list reg) diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 29254a4f..66b199cc 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -478,102 +478,6 @@ Section SOUNDNESS. rewrite negb_true_iff in H. intuition. Qed. - - Lemma reg_min_sound: - forall x y, (reg_min x y) = x \/ (reg_min x y) = y. - Proof. - intros; unfold reg_min. - destruct plt; auto. - Qed. - - Lemma reg_min_rec_sound : - forall (l : list reg) (before : reg), - In (reg_min_rec l before) l \/ - reg_min_rec l before = before. - Proof. - induction l; cbn. - { auto. } - intro bef. - destruct (IHl (reg_min bef a)). - { auto. } - rewrite H. - destruct (reg_min_sound bef a); auto. - Qed. - - Lemma pick_min_source_sound : - forall (l : list reg), - match pick_min_source l with - | Some x => In x l - | None => True - end. - Proof. - destruct l; cbn; trivial. - destruct (reg_min_rec_sound l r); auto. - Qed. - - Hint Resolve pick_min_source_sound : cse3. - - Theorem get_sources_sound : - forall l src rs m x, - (forall i eq, - In i l -> - eq_catalog ctx i = Some eq -> - sem_eq eq rs m) -> - (In src (get_sources (ctx := ctx) x l)) -> - rs # src = rs # x. - Proof. - induction l; cbn; intros until x; intros SEM IN. - contradiction. - destruct (eq_catalog ctx a) eqn:CATALOG. - 2: eauto using IHl; fail. - pose proof (SEM a e) as SEMeq. - destruct e; cbn in *. - destruct (is_smove eq_op && peq x eq_lhs) eqn:CORRECT. - 2: eauto using IHl; fail. - destruct eq_args. - eauto using IHl; fail. - destruct eq_args. - 2: eauto using IHl; fail. - cbn in IN. - destruct IN. - 2: eauto using IHl; fail. - rewrite andb_true_iff in CORRECT. - intuition. - destruct (peq x eq_lhs). - 2: discriminate. - subst eq_lhs. - destruct (is_smove eq_op). - 2: discriminate. - subst eq_op. - subst src. - cbn in H2. - symmetry. - assumption. - Qed. - - Theorem forward_move2_sound : - forall rel rs m x, - (sem_rel rel rs m) -> - rs # (forward_move2 (ctx := ctx) rel x) = rs # x. - Proof. - unfold forward_move2. - intros until x; intros REL. - pose proof (pick_min_source_sound (get_sources (ctx := ctx) x (PSet.elements (PSet.inter rel (eq_moves ctx x))))) as PICK. - destruct pick_min_source. - 2: reflexivity. - apply get_sources_sound with (l := (PSet.elements (PSet.inter rel (eq_moves ctx x)))) (m:=m). - 2: assumption. - intros i eq IN CATALOG. - rewrite PSet.elements_spec in IN. - rewrite PSet.ginter in IN. - rewrite andb_true_iff in IN. - destruct IN. - unfold sem_rel in REL. - apply REL with (i:=i); assumption. - Qed. - - Hint Resolve forward_move2_sound : cse3. - Lemma pick_source_sound : forall (l : list reg), @@ -589,12 +493,12 @@ Section SOUNDNESS. Hint Resolve pick_source_sound : cse3. - Theorem forward_move1_sound : + Theorem forward_move_sound : forall rel rs m x, (sem_rel rel rs m) -> - rs # (forward_move1 (ctx := ctx) rel x) = rs # x. + rs # (forward_move (ctx := ctx) rel x) = rs # x. Proof. - unfold sem_rel, forward_move1. + unfold sem_rel, forward_move. intros until x. intro REL. pose proof (pick_source_sound (PSet.elements (PSet.inter rel (eq_moves ctx x)))) as ELEMENT. @@ -623,17 +527,6 @@ Section SOUNDNESS. intuition congruence. Qed. - Hint Resolve forward_move1_sound : cse3. - - Theorem forward_move_sound : - forall rel rs m x, - (sem_rel rel rs m) -> - rs # (forward_move (ctx := ctx) rel x) = rs # x. - Proof. - unfold forward_move. - apply forward_move1_sound. - Qed. - Hint Resolve forward_move_sound : cse3. Theorem forward_move_l_sound : @@ -806,28 +699,6 @@ Section SOUNDNESS. + congruence. Qed. - - Lemma arglist_idem_write: - forall { A : Type} args (rs : Regmap.t A) dst, - (rs # dst <- (rs # dst)) ## args = rs ## args. - Proof. - induction args; trivial. - intros. cbn. - f_equal; trivial. - apply Regmap.gsident. - Qed. - - Lemma sem_rhs_idem_write: - forall sop args rs dst m v, - sem_rhs sop args rs m v -> - sem_rhs sop args (rs # dst <- (rs # dst)) m v. - Proof. - intros. - unfold sem_rhs in *. - rewrite arglist_idem_write. - assumption. - Qed. - Theorem oper2_sound: forall no dst sop args rel rs m v, sem_rel rel rs m -> @@ -855,17 +726,6 @@ Section SOUNDNESS. rewrite Regmap.gss. apply sem_rhs_depends_on_args_only; auto. } - intros INi. - destruct (PSet.contains rel e) eqn:CONTAINSe. - { pose proof (REL e {| eq_lhs := dst; eq_op := sop; eq_args := args |} CONTAINSe H) as RELe. - pose proof (REL i eq CONTAINS INi) as RELi. - unfold sem_eq in *. - cbn in RELe. - replace v with (rs # dst) by (eapply sem_rhs_det; eassumption). - rewrite Regmap.gsident. - apply sem_rhs_idem_write. - assumption. - } rewrite PSet.gaddo in CONTAINS by congruence. apply (kill_reg_sound rel rs m dst v REL i eq); auto. Qed. @@ -961,7 +821,11 @@ Section SOUNDNESS. subst. rewrite <- (forward_move_sound rel rs m r) by auto. apply move_sound; auto. - - destruct rhs_find as [src |] eqn:RHS_FIND. + - destruct (is_trivial_sym_op sop). + { + apply kill_reg_sound; auto. + } + destruct rhs_find as [src |] eqn:RHS_FIND. + destruct (Compopts.optim_CSE3_glb tt). * apply sem_rel_glb; split. ** pose proof (rhs_find_sound no sop (forward_move_l (ctx:=ctx) rel args) rel src rs m REL RHS_FIND) as SOUND. @@ -969,18 +833,12 @@ Section SOUNDNESS. 2: eassumption. rewrite <- (sem_rhs_det SOUND RHS). apply move_sound; auto. - ** apply sem_rel_glb; split. - *** apply oper1_sound; auto. - apply forward_move_rhs_sound; auto. - *** apply oper1_sound; auto. - * apply sem_rel_glb; split. ** apply oper1_sound; auto. apply forward_move_rhs_sound; auto. - ** apply oper1_sound; auto. - + apply sem_rel_glb; split. - * apply oper1_sound; auto. - apply forward_move_rhs_sound; auto. - * apply oper1_sound; auto. + * ** apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. + + apply oper1_sound; auto. + apply forward_move_rhs_sound; auto. Qed. Hint Resolve oper_sound : cse3. diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index a0361746..3fbc9912 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -63,7 +63,7 @@ Proof. destruct rel as [rel | ]; simpl; intros. 2: contradiction. eapply forward_move_sound; eauto. -Qed. + Qed. Lemma forward_move_l_b_sound : forall rel rs m x, @@ -447,6 +447,7 @@ Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'. +Proof. induction 1; intros S1' MS; inv MS. - (* Inop *) exists (State ts tf sp pc' rs m). split. @@ -462,12 +463,12 @@ Lemma step_simulation: destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op) (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. - * destruct (if (negb (Compopts.optim_CSE3_trivial_ops tt) && is_trivial_op op) + * destruct (if is_trivial_op op then None else rhs_find pc (SOp op) (subst_args (fst (preanalysis tenv f)) pc args) t) eqn:FIND. - ** destruct (negb (Compopts.optim_CSE3_trivial_ops tt) && is_trivial_op op). discriminate. + ** destruct (is_trivial_op op). discriminate. apply exec_Iop with (op := Omove) (args := r :: nil). TR_AT. subst instr'. |