diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Allocproof.v | 2 | ||||
-rw-r--r-- | backend/CSEproof.v | 2 | ||||
-rw-r--r-- | backend/CastOptim.v | 8 | ||||
-rw-r--r-- | backend/CastOptimproof.v | 2 | ||||
-rw-r--r-- | backend/Constprop.v | 13 | ||||
-rw-r--r-- | backend/Constpropproof.v | 2 | ||||
-rw-r--r-- | backend/Kildall.v | 70 | ||||
-rw-r--r-- | backend/LTL.v | 2 | ||||
-rw-r--r-- | backend/Linearizeproof.v | 2 | ||||
-rw-r--r-- | backend/RTL.v | 2 | ||||
-rw-r--r-- | backend/RTLgen.v | 2 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 3 | ||||
-rw-r--r-- | backend/RTLgenspec.v | 7 |
13 files changed, 53 insertions, 64 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 5a5e4c4d..daa53e54 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -165,7 +165,7 @@ Proof. apply agree_increasing with (live!!n). eapply DS.fixpoint_solution. unfold analyze in H; eauto. unfold RTL.successors, Kildall.successors_list. - rewrite PTree.gmap. rewrite H0. simpl. auto. + rewrite PTree.gmap1. rewrite H0. simpl. auto. auto. Qed. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index c5670e8d..275b9fd2 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -695,7 +695,7 @@ Proof. intros res FIXPOINT WF AT SUCC. assert (Numbering.ge res!!pc' (transfer f pc res!!pc)). eapply Solver.fixpoint_solution; eauto. - unfold successors_list, successors. rewrite PTree.gmap. + unfold successors_list, successors. rewrite PTree.gmap1. rewrite AT. auto. apply H. intros. rewrite PMap.gi. apply empty_numbering_satisfiable. diff --git a/backend/CastOptim.v b/backend/CastOptim.v index 545564d8..19d0065f 100644 --- a/backend/CastOptim.v +++ b/backend/CastOptim.v @@ -136,12 +136,12 @@ Module Approx <: SEMILATTICE_WITH_TOP. | Single, Single => Single | _, _ => Unknown end. - Lemma lub_commut: forall x y, eq (lub x y) (lub y x). + Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. - unfold lub, eq; intros. - destruct x; destruct y; auto. + unfold lub, ge; intros. + destruct x; destruct y; auto. Qed. - Lemma ge_lub_left: forall x y, ge (lub x y) x. + Lemma ge_lub_right: forall x y, ge (lub x y) y. Proof. unfold lub, ge; intros. destruct x; destruct y; auto. diff --git a/backend/CastOptimproof.v b/backend/CastOptimproof.v index d5076090..b04e061a 100644 --- a/backend/CastOptimproof.v +++ b/backend/CastOptimproof.v @@ -118,7 +118,7 @@ Proof. intros approxs; intros. apply regs_match_approx_increasing with (transfer f pc approxs!!pc). eapply DS.fixpoint_solution; eauto. - unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto. + unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto. auto. intros. rewrite PMap.gi. apply regs_match_approx_top. Qed. diff --git a/backend/Constprop.v b/backend/Constprop.v index 03966cdd..47c40e3e 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -87,12 +87,6 @@ Module Approx <: SEMILATTICE_WITH_TOP. | _, Novalue => x | _, _ => Unknown end. - Lemma lub_commut: forall x y, eq (lub x y) (lub y x). - Proof. - unfold lub, eq; intros. - case (eq_dec x y); case (eq_dec y x); intros; try congruence. - destruct x; destruct y; auto. - Qed. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. unfold lub; intros. @@ -100,6 +94,13 @@ Module Approx <: SEMILATTICE_WITH_TOP. apply ge_refl. apply eq_refl. destruct x; destruct y; unfold ge; tauto. Qed. + Lemma ge_lub_right: forall x y, ge (lub x y) y. + Proof. + unfold lub; intros. + case (eq_dec x y); intro. + apply ge_refl. subst. apply eq_refl. + destruct x; destruct y; unfold ge; tauto. + Qed. End Approx. Module D := LPMap Approx. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 714468aa..1dad5187 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -106,7 +106,7 @@ Proof. intros approxs; intros. apply regs_match_approx_increasing with (transfer f pc approxs!!pc). eapply DS.fixpoint_solution; eauto. - unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto. + unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto. auto. intros. rewrite PMap.gi. apply regs_match_approx_top. Qed. diff --git a/backend/Kildall.v b/backend/Kildall.v index 83206f78..e1e6ea53 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -344,14 +344,12 @@ Proof. ((st_in st) !! n) (L.lub (st_in st) !! n out). split. eapply L.ge_trans. apply L.ge_refl. apply H; auto. - eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. - apply L.ge_lub_left. + apply L.ge_lub_right. auto. simpl. split. rewrite PMap.gss. - eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. - apply L.ge_lub_left. + apply L.ge_lub_right. intros. rewrite PMap.gso; auto. Qed. @@ -506,8 +504,7 @@ Proof. elim H. elim H; intros. subst a. rewrite PMap.gss. - eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. - apply L.ge_lub_left. + apply L.ge_lub_right. destruct a. rewrite PMap.gsspec. case (peq n p); intro. subst p. apply L.ge_trans with (start_state_in ep)!!n. apply L.ge_lub_left. auto. @@ -1168,49 +1165,41 @@ End BBlock_solver. greatest node in the working list. For backward analysis, we will similarly pick the smallest node in the working list. *) -Require Import FSets. -Require Import FSetAVL. -Require Import Ordered. - -Module PositiveSet := FSetAVL.Make(OrderedPositive). -Module PositiveSetFacts := FSetFacts.Facts(PositiveSet). +Require Import Heaps. Module NodeSetForward <: NODE_SET. - Definition t := PositiveSet.t. - Definition add (n: positive) (s: t) : t := PositiveSet.add n s. + Definition t := PHeap.t. + Definition add (n: positive) (s: t) : t := PHeap.insert n s. Definition pick (s: t) := - match PositiveSet.max_elt s with - | Some n => Some(n, PositiveSet.remove n s) + match PHeap.findMax s with + | Some n => Some(n, PHeap.deleteMax s) | None => None end. Definition initial (successors: PTree.t (list positive)) := - PTree.fold (fun s pc scs => PositiveSet.add pc s) successors PositiveSet.empty. - Definition In := PositiveSet.In. + PTree.fold (fun s pc scs => PHeap.insert pc s) successors PHeap.empty. + Definition In := PHeap.In. Lemma add_spec: forall n n' s, In n' (add n s) <-> n = n' \/ In n' s. Proof. - intros. exact (PositiveSetFacts.add_iff s n n'). + intros. rewrite PHeap.In_insert. unfold In. intuition. Qed. Lemma pick_none: forall s n, pick s = None -> ~In n s. Proof. - intros until n; unfold pick. caseEq (PositiveSet.max_elt s); intros. + intros until n; unfold pick. caseEq (PHeap.findMax s); intros. congruence. - apply PositiveSet.max_elt_3. auto. + apply PHeap.findMax_empty. auto. Qed. Lemma pick_some: forall s n s', pick s = Some(n, s') -> forall n', In n' s <-> n = n' \/ In n' s'. Proof. - intros until s'; unfold pick. caseEq (PositiveSet.max_elt s); intros. - inversion H0; clear H0; subst. - split; intros. - destruct (peq n n'). auto. right. apply PositiveSet.remove_2; assumption. - elim H0; intro. subst n'. apply PositiveSet.max_elt_1. auto. - apply PositiveSet.remove_3 with n; assumption. + intros until s'; unfold pick. caseEq (PHeap.findMax s); intros. + inv H0. + generalize (PHeap.In_deleteMax s n n' H). unfold In. intuition. congruence. Qed. @@ -1233,39 +1222,36 @@ Module NodeSetForward <: NODE_SET. End NodeSetForward. Module NodeSetBackward <: NODE_SET. - Definition t := PositiveSet.t. - Definition add (n: positive) (s: t) : t := PositiveSet.add n s. + Definition t := PHeap.t. + Definition add (n: positive) (s: t) : t := PHeap.insert n s. Definition pick (s: t) := - match PositiveSet.min_elt s with - | Some n => Some(n, PositiveSet.remove n s) + match PHeap.findMin s with + | Some n => Some(n, PHeap.deleteMin s) | None => None end. Definition initial (successors: PTree.t (list positive)) := - PTree.fold (fun s pc scs => PositiveSet.add pc s) successors PositiveSet.empty. - Definition In := PositiveSet.In. + PTree.fold (fun s pc scs => PHeap.insert pc s) successors PHeap.empty. + Definition In := PHeap.In. Lemma add_spec: forall n n' s, In n' (add n s) <-> n = n' \/ In n' s. Proof NodeSetForward.add_spec. - + Lemma pick_none: forall s n, pick s = None -> ~In n s. Proof. - intros until n; unfold pick. caseEq (PositiveSet.min_elt s); intros. + intros until n; unfold pick. caseEq (PHeap.findMin s); intros. congruence. - apply PositiveSet.min_elt_3. auto. + apply PHeap.findMin_empty. auto. Qed. Lemma pick_some: forall s n s', pick s = Some(n, s') -> forall n', In n' s <-> n = n' \/ In n' s'. Proof. - intros until s'; unfold pick. caseEq (PositiveSet.min_elt s); intros. - inversion H0; clear H0; subst. - split; intros. - destruct (peq n n'). auto. right. apply PositiveSet.remove_2; assumption. - elim H0; intro. subst n'. apply PositiveSet.min_elt_1. auto. - apply PositiveSet.remove_3 with n; assumption. + intros until s'; unfold pick. caseEq (PHeap.findMin s); intros. + inv H0. + generalize (PHeap.In_deleteMin s n n' H). unfold In. intuition. congruence. Qed. diff --git a/backend/LTL.v b/backend/LTL.v index 2eff67cd..a68352fc 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -290,4 +290,4 @@ Definition successors_instr (i: instruction) : list node := end. Definition successors (f: function): PTree.t (list node) := - PTree.map (fun pc i => successors_instr i) f.(fn_code). + PTree.map1 successors_instr f.(fn_code). diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index df750008..abc497ec 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -128,7 +128,7 @@ Proof. assert (LBoolean.ge reach!!pc' reach!!pc). change (reach!!pc) with ((fun pc r => r) pc (reach!!pc)). eapply DS.fixpoint_solution. eexact H. - unfold Kildall.successors_list, successors. rewrite PTree.gmap. + unfold Kildall.successors_list, successors. rewrite PTree.gmap1. rewrite H0; auto. elim H3; intro. congruence. auto. intros. apply PMap.gi. diff --git a/backend/RTL.v b/backend/RTL.v index 1c309a0c..208c7b13 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -368,7 +368,7 @@ Definition successors_instr (i: instruction) : list node := end. Definition successors (f: function) : PTree.t (list node) := - PTree.map (fun pc i => successors_instr i) f.(fn_code). + PTree.map1 successors_instr f.(fn_code). (** Transformation of a RTL function instruction by instruction. This applies a given transformation function to all instructions diff --git a/backend/RTLgen.v b/backend/RTLgen.v index e9184494..a9c8f97c 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -591,7 +591,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do n1 <- reserve_instr; do n2 <- transl_stmt map sbody n1 nexits ngoto nret rret; do xx <- update_instr n1 (Inop n2); - ret n1 + add_instr (Inop n2) | Sblock sbody => transl_stmt map sbody nd (nd :: nexits) ngoto nret rret | Sexit n => diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index b49b671a..24f8c1a7 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1069,7 +1069,7 @@ Proof. inv H2. eapply IHs2; eauto. (* loop *) intros. inversion H1; subst. - eapply IHs; eauto. econstructor; eauto. + eapply IHs; eauto. econstructor; eauto. econstructor; eauto. (* block *) intros. inv H1. eapply IHs; eauto. econstructor; eauto. @@ -1216,6 +1216,7 @@ Proof. left. apply plus_one. eapply exec_Inop; eauto. econstructor; eauto. econstructor; eauto. + econstructor; eauto. (* block *) inv TS. diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 44e7c418..9b2e63e8 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -885,9 +885,10 @@ Inductive tr_stmt (c: code) (map: mapping): tr_stmt c map sfalse nfalse nd nexits ngoto nret rret -> tr_condition c map nil a ns ntrue nfalse -> tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits ngoto nret rret - | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop, - tr_stmt c map sbody nloop ns nexits ngoto nret rret -> + | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop nend, + tr_stmt c map sbody nloop nend nexits ngoto nret rret -> c!ns = Some(Inop nloop) -> + c!nend = Some(Inop nloop) -> tr_stmt c map (Sloop sbody) ns nd nexits ngoto nret rret | tr_Sblock: forall sbody ns nd nexits ngoto nret rret, tr_stmt c map sbody ns nd (nd :: nexits) ngoto nret rret -> @@ -1294,7 +1295,7 @@ Proof. econstructor. apply tr_stmt_incr with s1; auto. eapply IHstmt; eauto with rtlg. - eauto with rtlg. + eauto with rtlg. eauto with rtlg. (* Sblock *) econstructor. eapply IHstmt; eauto with rtlg. |