diff options
-rw-r--r-- | backend/CSE3analysisproof.v | 81 | ||||
-rw-r--r-- | backend/CSE3proof.v | 37 |
2 files changed, 115 insertions, 3 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index cd27a506..94d3142f 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -120,7 +120,14 @@ Definition xlget_kills (eqs : list (eq_id * equation)) (m : Regmap.t PSet.t) : Regmap.t PSet.t := List.fold_left (fun already (item : eq_id * equation) => add_i_j (eq_lhs (snd item)) (fst item) - (add_ilist_j (eq_args (snd item)) (fst item) already)) eqs m. + (add_ilist_j (eq_args (snd item)) (fst item) already)) eqs m. + + +Definition xlget_mem_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t := +(fold_left + (fun (a : PSet.t) (p : positive * equation) => + if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a) + eqs m). Lemma xlget_kills_monotone : forall eqs m i j, @@ -134,6 +141,24 @@ Qed. Hint Resolve xlget_kills_monotone : cse3. +Lemma xlget_mem_kills_monotone : + forall eqs m j, + PSet.contains m j = true -> + PSet.contains (xlget_mem_kills eqs m) j = true. +Proof. + induction eqs; simpl; trivial. + intros. + destruct eq_depends_on_mem. + - apply IHeqs. + destruct (peq (fst a) j). + + subst j. apply PSet.gadds. + + rewrite PSet.gaddo by congruence. + trivial. + - auto. +Qed. + +Hint Resolve xlget_mem_kills_monotone : cse3. + Lemma xlget_kills_has_lhs : forall eqs m lhs sop args j, In (j, {| eq_lhs := lhs; @@ -243,6 +268,60 @@ Qed. Hint Resolve context_from_hints_get_kills_has_arg : cse3. +Lemma xlget_kills_has_eq_depends_on_mem : + forall eqs eq j m, + In (j, eq) eqs -> + eq_depends_on_mem eq = true -> + PSet.contains (xlget_mem_kills eqs m) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros. + destruct H. + { subst a. + simpl. + rewrite H0. + apply xlget_mem_kills_monotone. + apply PSet.gadds. + } + eauto. +Qed. + +Hint Resolve xlget_kills_has_eq_depends_on_mem : cse3. + +Lemma get_kills_has_eq_depends_on_mem : + forall eqs eq j, + PTree.get j eqs = Some eq -> + eq_depends_on_mem eq = true -> + PSet.contains (get_mem_kills eqs) j = true. +Proof. + intros. + unfold get_mem_kills. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : PSet.t) (p : positive * equation) => + if eq_depends_on_mem (snd p) then PSet.add (fst p) a else a) + (PTree.elements eqs) PSet.empty) + with (xlget_mem_kills (PTree.elements eqs) PSet.empty). + eapply xlget_kills_has_eq_depends_on_mem. + apply PTree.elements_correct. + eassumption. + trivial. +Qed. + +Lemma context_from_hints_get_kills_has_eq_depends_on_mem : + forall hints eq j, + PTree.get j (hint_eq_catalog hints) = Some eq -> + eq_depends_on_mem eq = true -> + PSet.contains (eq_kill_mem (context_from_hints hints) tt) j = true. +Proof. + intros. + simpl. + eapply get_kills_has_eq_depends_on_mem; eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_eq_depends_on_mem : cse3. + Definition eq_involves (eq : equation) (i : reg) := i = (eq_lhs eq) \/ In i (eq_args eq). diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 3cc48cca..6744ee93 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -377,6 +377,31 @@ Proof. Qed. Hint Resolve sem_rhs_sload : cse3. + +Lemma sem_rhs_sload_notrap1 : + forall sp chunk addr rs args m, + eval_addressing ge sp addr rs ## args = None -> + sem_rhs (genv:=ge) (sp:=sp) (SLoad chunk addr) args rs m Vundef. +Proof. + intros. simpl. + rewrite H. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sload_notrap1 : cse3. + +Lemma sem_rhs_sload_notrap2 : + forall sp chunk addr rs args m a, + eval_addressing ge sp addr rs ## args = Some a -> + Mem.loadv chunk m a = None -> + sem_rhs (genv:=ge) (sp:=sp) (SLoad chunk addr) args rs m Vundef. +Proof. + intros. simpl. + rewrite H. rewrite H0. + reflexivity. +Qed. + +Hint Resolve sem_rhs_sload_notrap2 : cse3. Ltac IND_STEP := match goal with @@ -432,18 +457,26 @@ Proof. exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. + admit. + econstructor; eauto. - apply wt_undef; assumption. + * apply wt_undef; assumption. + * IND_STEP. + apply oper_sound; eauto with cse3. + - (* Iload notrap2 *) exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. + admit. + econstructor; eauto. - apply wt_undef; assumption. + * apply wt_undef; assumption. + * IND_STEP. + apply oper_sound; eauto with cse3. + - (* Istore *) exists (State ts tf sp pc' rs m'). split. + eapply exec_Istore; try eassumption. * TR_AT. reflexivity. * admit. + econstructor; eauto. + IND_STEP. + - (* Icall *) destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]]. econstructor. split. |