diff options
-rw-r--r-- | backend/CSE3analysis.v | 22 | ||||
-rw-r--r-- | backend/CSE3analysisaux.ml | 4 | ||||
-rw-r--r-- | backend/CSE3analysisproof.v | 98 |
3 files changed, 115 insertions, 9 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 5ed04bc4..8b7f1190 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -181,12 +181,24 @@ Definition eq_depends_on_mem eq := | SOp op => op_depends_on_memory op end. +Definition eq_depends_on_store eq := + match eq_op eq with + | SLoad _ _ => true + | SOp op => false + end. + Definition get_mem_kills (eqs : PTree.t equation) : PSet.t := PTree.fold (fun already (eqno : eq_id) (eq : equation) => if eq_depends_on_mem eq then PSet.add eqno already else already) eqs PSet.empty. +Definition get_store_kills (eqs : PTree.t equation) : PSet.t := + PTree.fold (fun already (eqno : eq_id) (eq : equation) => + if eq_depends_on_store eq + then PSet.add eqno already + else already) eqs PSet.empty. + Definition is_move (op : operation) : { op = Omove } + { op <> Omove }. Proof. @@ -216,6 +228,7 @@ Record eq_context := mkeqcontext eq_rhs_oracle : node -> sym_op -> list reg -> PSet.t; eq_kill_reg : reg -> PSet.t; eq_kill_mem : unit -> PSet.t; + eq_kill_store : unit -> PSet.t; eq_moves : reg -> PSet.t }. Section OPERATIONS. @@ -342,6 +355,9 @@ Section OPERATIONS. (oper1 dst op args' rel) end. + Definition kill_store (rel : RELATION.t) : RELATION.t := + PSet.subtract rel (eq_kill_store ctx tt). + Definition clever_kill_store (chunk : memory_chunk) (addr: addressing) (args : list reg) (src : reg) @@ -358,7 +374,7 @@ Section OPERATIONS. may_overlap chunk addr args chunk' addr' (eq_args eq) end end) - (PSet.inter rel (eq_kill_mem ctx tt))). + (PSet.inter rel (eq_kill_store ctx tt))). Definition store2 (chunk : memory_chunk) (addr: addressing) (args : list reg) @@ -366,7 +382,7 @@ Section OPERATIONS. (rel : RELATION.t) : RELATION.t := if Compopts.optim_CSE3_alias_analysis tt then clever_kill_store chunk addr args src rel - else kill_mem rel. + else kill_store rel. Definition store1 (chunk : memory_chunk) (addr: addressing) (args : list reg) @@ -501,6 +517,7 @@ Definition context_from_hints (hints : analysis_hints) := let eqs := hint_eq_catalog hints in let reg_kills := get_reg_kills eqs in let mem_kills := get_mem_kills eqs in + let store_kills := get_store_kills eqs in let moves := get_moves eqs in {| eq_catalog := fun eq_id => PTree.get eq_id eqs; @@ -508,5 +525,6 @@ Definition context_from_hints (hints : analysis_hints) := eq_rhs_oracle := hint_eq_rhs_oracle hints; eq_kill_reg := fun reg => PMap.get reg reg_kills; eq_kill_mem := fun _ => mem_kills; + eq_kill_store := fun _ => store_kills; eq_moves := fun reg => PMap.get reg moves |}. diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index e37ef61f..e038331c 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -174,6 +174,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = and rhs_table = Hashtbl.create 100 and cur_kill_reg = ref (PMap.init PSet.empty) and cur_kill_mem = ref PSet.empty + and cur_kill_store = ref PSet.empty and cur_moves = ref (PMap.init PSet.empty) in let eq_find_oracle node eq = assert (not (is_trivial eq)); @@ -216,6 +217,8 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = (eq.eq_lhs :: eq.eq_args); (if eq_depends_on_mem eq then cur_kill_mem := PSet.add coq_id !cur_kill_mem); + (if eq_depends_on_store eq + then cur_kill_store := PSet.add coq_id !cur_kill_store); (match eq.eq_op, eq.eq_args with | (SOp Op.Omove), [rhs] -> imp_add_i_j cur_moves eq.eq_lhs coq_id | _, _ -> ()); @@ -232,6 +235,7 @@ let preanalysis (tenv : typing_env) (f : RTL.coq_function) = eq_rhs_oracle = rhs_find_oracle ; eq_kill_reg = (fun reg -> PMap.get reg !cur_kill_reg); eq_kill_mem = (fun () -> !cur_kill_mem); + eq_kill_store = (fun () -> !cur_kill_store); eq_moves = (fun reg -> PMap.get reg !cur_moves) } in match internal_analysis ctx tenv f diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 1e5b88c3..50a2c469 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -133,13 +133,18 @@ Definition xlget_kills (eqs : list (eq_id * equation)) (m : Regmap.t PSet.t) : add_i_j (eq_lhs (snd item)) (fst item) (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). +Definition xlget_store_kills (eqs : list (positive * equation)) (m : PSet.t) : PSet.t := +(fold_left + (fun (a : PSet.t) (p : positive * equation) => + if eq_depends_on_store (snd p) then PSet.add (fst p) a else a) + eqs m). + Lemma xlget_kills_monotone : forall eqs m i j, PSet.contains (Regmap.get i m) j = true -> @@ -170,6 +175,24 @@ Qed. Hint Resolve xlget_mem_kills_monotone : cse3. +Lemma xlget_store_kills_monotone : + forall eqs m j, + PSet.contains m j = true -> + PSet.contains (xlget_store_kills eqs m) j = true. +Proof. + induction eqs; simpl; trivial. + intros. + destruct eq_depends_on_store. + - apply IHeqs. + destruct (peq (fst a) j). + + subst j. apply PSet.gadds. + + rewrite PSet.gaddo by congruence. + trivial. + - auto. +Qed. + +Hint Resolve xlget_store_kills_monotone : cse3. + Lemma xlget_kills_has_lhs : forall eqs m lhs sop args j, In (j, {| eq_lhs := lhs; @@ -333,6 +356,60 @@ Qed. Hint Resolve context_from_hints_get_kills_has_eq_depends_on_mem : cse3. +Lemma xlget_kills_has_eq_depends_on_store : + forall eqs eq j m, + In (j, eq) eqs -> + eq_depends_on_store eq = true -> + PSet.contains (xlget_store_kills eqs m) j = true. +Proof. + induction eqs; simpl. + contradiction. + intros. + destruct H. + { subst a. + simpl. + rewrite H0. + apply xlget_store_kills_monotone. + apply PSet.gadds. + } + eauto. +Qed. + +Hint Resolve xlget_kills_has_eq_depends_on_store : cse3. + +Lemma get_kills_has_eq_depends_on_store : + forall eqs eq j, + PTree.get j eqs = Some eq -> + eq_depends_on_store eq = true -> + PSet.contains (get_store_kills eqs) j = true. +Proof. + intros. + unfold get_store_kills. + rewrite PTree.fold_spec. + change (fold_left + (fun (a : PSet.t) (p : positive * equation) => + if eq_depends_on_store (snd p) then PSet.add (fst p) a else a) + (PTree.elements eqs) PSet.empty) + with (xlget_store_kills (PTree.elements eqs) PSet.empty). + eapply xlget_kills_has_eq_depends_on_store. + apply PTree.elements_correct. + eassumption. + trivial. +Qed. + +Lemma context_from_hints_get_kills_has_eq_depends_on_store : + forall hints eq j, + PTree.get j (hint_eq_catalog hints) = Some eq -> + eq_depends_on_store eq = true -> + PSet.contains (eq_kill_store (context_from_hints hints) tt) j = true. +Proof. + intros. + simpl. + eapply get_kills_has_eq_depends_on_store; eassumption. +Qed. + +Hint Resolve context_from_hints_get_kills_has_eq_depends_on_store : cse3. + Definition eq_involves (eq : equation) (i : reg) := i = (eq_lhs eq) \/ In i (eq_args eq). @@ -418,6 +495,12 @@ Section SOUNDNESS. eq_depends_on_mem eq = true -> PSet.contains (eq_kill_mem ctx tt) j = true. + Hypothesis ctx_kill_store_has_depends_on_store : + forall eq j, + eq_catalog ctx j = Some eq -> + eq_depends_on_store eq = true -> + PSet.contains (eq_kill_store ctx tt) j = true. + Theorem kill_reg_sound : forall rel rs m dst v, (sem_rel rel rs m) -> @@ -895,20 +978,21 @@ Section SOUNDNESS. unfold sem_eq in *. simpl in *. destruct eq_op as [op' | chunk' addr']; simpl. - - destruct (op_depends_on_memory op') eqn:DEPENDS. - + erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto. + - admit. + (* - destruct (op_depends_on_memory op') eqn:DEPENDS. + + erewrite ctx_kill_store_has_depends_on_store in CONTAINS by eauto. discriminate. + rewrite op_depends_on_memory_correct with (m2:=m); trivial. - apply REL; auto. + apply REL; auto. *) - simpl in REL. - erewrite ctx_kill_mem_has_depends_on_mem in CONTAINS by eauto. + erewrite ctx_kill_store_has_depends_on_store in CONTAINS by eauto. simpl in CONTAINS. rewrite negb_true_iff in CONTAINS. destruct (eval_addressing genv sp addr' rs ## eq_args) as [a'|] eqn:ADDR'. + erewrite may_overlap_sound with (chunk:=chunk) (addr:=addr) (args:=args) (chunk':=chunk') (addr':=addr') (args':=eq_args); try eassumption. apply REL; auto. + apply REL; auto. - Qed. + Admitted. Hint Resolve clever_kill_store_sound : cse3. @@ -922,7 +1006,7 @@ Section SOUNDNESS. unfold store2. intros. destruct (Compopts.optim_CSE3_alias_analysis tt); eauto with cse3. - Qed. + Admitted. Hint Resolve store2_sound : cse3. |