diff options
-rw-r--r-- | backend/CSE3.v | 2 | ||||
-rw-r--r-- | backend/CSE3analysis.v | 39 | ||||
-rw-r--r-- | backend/CSE3analysisproof.v | 107 | ||||
-rw-r--r-- | backend/CSE3proof.v | 7 | ||||
-rw-r--r-- | extraction/extraction.v | 2 |
5 files changed, 109 insertions, 48 deletions
diff --git a/backend/CSE3.v b/backend/CSE3.v index df1c2bfc..58e179e2 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 is_trivial_op op then None else find_op_in_fmap fmap pc op args') with + 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 | 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 cd7e3d84..34df644e 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -227,29 +227,44 @@ Section OPERATIONS. Definition kill_mem (rel : RELATION.t) : RELATION.t := PSet.subtract rel (eq_kill_mem ctx tt). - Definition pick_source (l : list reg) := (* todo: take min? *) + 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) := match l with - | h::t => Some h + | h::t => Some (reg_min_rec t h) | nil => None end. - - 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 => + + 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 - | _ => x + | src::nil => src :: (get_sources x others) + | _ => get_sources x others end - else x - | _ => x + else get_sources x others + | _ => get_sources x others end end. - + + Definition forward_move (rel : RELATION.t) (x : reg) : reg := + match pick_source (get_sources x (PSet.elements (PSet.inter rel (eq_moves ctx x)))) with + | None => x + | Some src => src + end. + Definition forward_move_l (rel : RELATION.t) : list reg -> list reg := List.map (forward_move rel). diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index ea4d37ca..12048010 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -478,6 +478,27 @@ 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_source_sound : forall (l : list reg), @@ -486,47 +507,71 @@ Section SOUNDNESS. | None => True end. Proof. - unfold pick_source. - destruct l; simpl; trivial. - left; trivial. + destruct l; cbn; trivial. + destruct (reg_min_rec_sound l r); auto. Qed. - + Hint Resolve pick_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_move_sound : forall rel rs m x, (sem_rel rel rs m) -> rs # (forward_move (ctx := ctx) rel x) = rs # x. Proof. - 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. - destruct (pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x)))). - 2: reflexivity. - destruct (eq_catalog ctx r) as [eq | ] eqn:CATALOG. - 2: reflexivity. - specialize REL with (i := r) (eq0 := eq). - destruct (is_smove (eq_op eq)) as [MOVE | ]. - 2: reflexivity. - destruct (peq x (eq_lhs eq)). + unfold forward_move. + intros until x; intros REL. + pose proof (pick_source_sound (get_sources (ctx := ctx) x (PSet.elements (PSet.inter rel (eq_moves ctx x))))) as PICK. + destruct pick_source. 2: reflexivity. - simpl. - subst x. - rewrite PSet.elements_spec in ELEMENT. - rewrite PSet.ginter in ELEMENT. - rewrite andb_true_iff in ELEMENT. - unfold sem_eq in REL. - rewrite MOVE in REL. - simpl in REL. - destruct (eq_args eq) as [ | h t]. - reflexivity. - destruct t. - 2: reflexivity. - simpl in REL. - intuition congruence. + 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_move_sound : cse3. Theorem forward_move_l_sound : diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 3fbc9912..a0361746 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,7 +447,6 @@ 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. @@ -463,12 +462,12 @@ Proof. 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 is_trivial_op op + * destruct (if (negb (Compopts.optim_CSE3_trivial_ops tt) && is_trivial_op op) then None else rhs_find pc (SOp op) (subst_args (fst (preanalysis tenv f)) pc args) t) eqn:FIND. - ** destruct (is_trivial_op op). discriminate. + ** destruct (negb (Compopts.optim_CSE3_trivial_ops tt) && is_trivial_op op). discriminate. apply exec_Iop with (op := Omove) (args := r :: nil). TR_AT. subst instr'. diff --git a/extraction/extraction.v b/extraction/extraction.v index bd396cd8..c5fa7a62 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -127,6 +127,8 @@ Extract Constant Compopts.optim_CSE3_across_merges => "fun _ -> !Clflags.option_fcse3_across_merges". Extract Constant Compopts.optim_CSE3_glb => "fun _ -> !Clflags.option_fcse3_glb". +Extract Constant Compopts.optim_CSE3_trivial_ops => + "fun _ -> !Clflags.option_fcse3_trivial_ops". Extract Constant Compopts.optim_move_loop_invariants => "fun _ -> !Clflags.option_fmove_loop_invariants". |