diff options
| -rw-r--r-- | arm/Op.v | 1 | ||||
| -rw-r--r-- | backend/CSE3analysis.v | 22 | ||||
| -rw-r--r-- | backend/CSE3analysisaux.ml | 4 | ||||
| -rw-r--r-- | backend/CSE3analysisproof.v | 143 | ||||
| -rw-r--r-- | common/Values.v | 1 | ||||
| -rw-r--r-- | kvx/Op.v | 1 |
6 files changed, 161 insertions, 11 deletions
@@ -751,7 +751,6 @@ Proof. auto. Qed. - Lemma op_valid_pointer_eq: forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> 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..b298ea65 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) -> @@ -574,6 +657,55 @@ Section SOUNDNESS. Hint Resolve kill_mem_sound : cse3. + (* TODO: shouldn't this already be proved somewhere else? *) + Lemma store_preserves_validity: + forall m m' wchunk a v + (STORE : Mem.storev wchunk m a v = Some m') + (b : block) (z : Z), + Mem.valid_pointer m' b z = Mem.valid_pointer m b z. + Proof. + unfold Mem.storev. + intros. + destruct a; try discriminate. + Local Transparent Mem.store. + unfold Mem.store in STORE. + destruct Mem.valid_access_dec in STORE. + 2: discriminate. + inv STORE. + reflexivity. + Qed. + + Hint Resolve store_preserves_validity : cse3. + + Theorem kill_store_sound : + forall rel rs m m' wchunk a v, + (sem_rel rel rs m) -> + (Mem.storev wchunk m a v = Some m') -> + (sem_rel (kill_store (ctx:=ctx) rel) rs m'). + Proof. + unfold sem_rel, sem_eq, sem_rhs, kill_store. + intros until v. + intros REL STORE i eq. + specialize REL with (i := i) (eq0 := eq). + intros SUBTRACT CATALOG. + rewrite PSet.gsubtract in SUBTRACT. + rewrite andb_true_iff in SUBTRACT. + intuition. + destruct (eq_op eq) as [op | chunk addr] eqn:OP. + - rewrite op_valid_pointer_eq with (m2 := m). + assumption. + eapply store_preserves_validity; eauto. + - specialize ctx_kill_store_has_depends_on_store with (eq0 := eq) (j := i). + destruct eq as [lhs op args]; simpl in *. + rewrite OP in ctx_kill_store_has_depends_on_store. + rewrite negb_true_iff in H0. + rewrite OP in CATALOG. + intuition. + congruence. + Qed. + + Hint Resolve kill_store_sound : cse3. + Theorem eq_find_sound: forall no eq id, eq_find (ctx := ctx) no eq = Some id -> @@ -895,13 +1027,12 @@ 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. - discriminate. - + rewrite op_depends_on_memory_correct with (m2:=m); trivial. + - rewrite op_valid_pointer_eq with (m2 := m). + + cbn in *. apply REL; auto. + + eapply store_preserves_validity; eauto. - 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'. diff --git a/common/Values.v b/common/Values.v index 65b0b5ef..41138e8e 100644 --- a/common/Values.v +++ b/common/Values.v @@ -2727,4 +2727,3 @@ Proof. destruct v2; try congruence; rewrite !EQ; auto. Qed. - @@ -1258,7 +1258,6 @@ Proof. erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. Qed. - (** Global variables mentioned in an operation or addressing mode *) Definition globals_addressing (addr: addressing) : list ident := |