From c98440cad6b7a9c793aded892ec61a8ed50cac28 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 2 Mar 2007 15:43:35 +0000 Subject: Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de Lattice pour utiliser une notion d'egalite possiblement differente de =. Adaptation de Kildall et de ses utilisateurs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- .depend | 12 +- Makefile | 2 +- backend/Allocation.v | 4 +- backend/Allocproof.v | 87 ++++---- backend/Coloring.v | 6 +- backend/Coloringproof.v | 131 ++++++------ backend/Constprop.v | 31 ++- backend/InterfGraph.v | 44 +++-- backend/Kildall.v | 31 +-- backend/Linearize.v | 1 - backend/Registers.v | 6 +- cfrontend/Cminorgen.v | 6 +- cfrontend/Cminorgenproof.v | 2 +- extraction/.depend | 257 ++++++++++++------------ extraction/Makefile | 17 +- extraction/convert | 8 + lib/Lattice.v | 199 +++++++++++++++---- lib/Maps.v | 82 ++++++++ lib/Sets.v | 189 ------------------ lib/union_find.v | 484 --------------------------------------------- test/c/Makefile | 5 + 21 files changed, 594 insertions(+), 1010 deletions(-) create mode 100755 extraction/convert delete mode 100644 lib/Sets.v delete mode 100644 lib/union_find.v diff --git a/.depend b/.depend index 1571fa79..5262e32b 100644 --- a/.depend +++ b/.depend @@ -1,7 +1,5 @@ lib/Coqlib.vo: lib/Coqlib.v lib/Maps.vo: lib/Maps.v lib/Coqlib.vo -lib/Sets.vo: lib/Sets.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo -lib/union_find.vo: lib/union_find.v lib/Lattice.vo: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Iteration.vo: lib/Iteration.v lib/Coqlib.vo @@ -18,7 +16,7 @@ backend/Op.vo: backend/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floa backend/Cminor.vo: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Mem.vo backend/Op.vo common/Globalenvs.vo backend/Cmconstr.vo: backend/Cmconstr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo backend/Op.vo common/Globalenvs.vo backend/Cminor.vo backend/Cmconstrproof.vo: backend/Cmconstrproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo backend/Op.vo common/Globalenvs.vo backend/Cminor.vo backend/Cmconstr.vo -backend/Registers.vo: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Sets.vo +backend/Registers.vo: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Ordered.vo backend/RTL.vo: backend/RTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTLgen.vo: backend/RTLgen.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo backend/RTLgenproof1.vo: backend/RTLgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/Cminor.vo backend/RTL.vo backend/RTLgen.vo @@ -37,7 +35,7 @@ backend/InterfGraph.vo: backend/InterfGraph.v lib/Coqlib.vo lib/Maps.vo lib/Orde backend/Coloring.vo: backend/Coloring.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo backend/Coloringproof.vo: backend/Coloringproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/InterfGraph.vo backend/Coloring.vo backend/Parallelmove.vo: backend/Parallelmove.v lib/Coqlib.vo lib/Parmov.vo common/Values.vo common/Events.vo common/AST.vo backend/Locations.vo backend/Conventions.vo -backend/Allocation.vo: backend/Allocation.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Parallelmove.vo backend/LTL.vo +backend/Allocation.vo: backend/Allocation.v lib/Coqlib.vo lib/Maps.vo lib/Lattice.vo common/AST.vo lib/Integers.vo common/Values.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Kildall.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Parallelmove.vo backend/LTL.vo backend/Allocproof.vo: backend/Allocproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/RTLtyping.vo backend/Locations.vo backend/Conventions.vo backend/Coloring.vo backend/Coloringproof.vo backend/Parallelmove.vo backend/Allocation.vo backend/LTL.vo backend/Alloctyping.vo: backend/Alloctyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/Registers.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo backend/Coloring.vo backend/Coloringproof.vo backend/Allocation.vo backend/Allocproof.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/Conventions.vo backend/Parallelmove.vo backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo @@ -45,7 +43,7 @@ backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo co backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Linear.vo: backend/Linear.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo backend/Lineartyping.vo: backend/Lineartyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/Linear.vo backend/Conventions.vo -backend/Linearize.vo: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo common/AST.vo common/Values.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Kildall.vo lib/Lattice.vo +backend/Linearize.vo: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Kildall.vo lib/Lattice.vo backend/Linearizeproof.vo: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Linearize.vo lib/Lattice.vo backend/Linearizetyping.vo: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Linear.vo backend/Linearize.vo backend/LTLtyping.vo backend/Lineartyping.vo backend/Conventions.vo backend/Mach.vo: backend/Mach.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/Conventions.vo @@ -67,5 +65,5 @@ cfrontend/Cshmgenproof1.vo: cfrontend/Cshmgenproof1.v lib/Coqlib.vo lib/Maps.vo cfrontend/Cshmgenproof2.vo: cfrontend/Cshmgenproof2.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Ctyping.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo cfrontend/Cshmgenproof1.vo cfrontend/Cshmgenproof3.vo: cfrontend/Cshmgenproof3.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/AST.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Ctyping.vo cfrontend/Csharpminor.vo cfrontend/Cshmgen.vo cfrontend/Cshmgenproof1.vo cfrontend/Cshmgenproof2.vo cfrontend/Csharpminor.vo: cfrontend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo -cfrontend/Cminorgen.vo: cfrontend/Cminorgen.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo common/AST.vo lib/Integers.vo common/Mem.vo cfrontend/Csharpminor.vo backend/Op.vo backend/Cminor.vo backend/Cmconstr.vo -cfrontend/Cminorgenproof.vo: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Maps.vo lib/Sets.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo cfrontend/Csharpminor.vo backend/Op.vo backend/Cminor.vo backend/Cmconstr.vo cfrontend/Cminorgen.vo backend/Cmconstrproof.vo +cfrontend/Cminorgen.vo: cfrontend/Cminorgen.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Mem.vo cfrontend/Csharpminor.vo backend/Op.vo backend/Cminor.vo backend/Cmconstr.vo +cfrontend/Cminorgenproof.vo: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo cfrontend/Csharpminor.vo backend/Op.vo backend/Cminor.vo backend/Cmconstr.vo cfrontend/Cminorgen.vo backend/Cmconstrproof.vo diff --git a/Makefile b/Makefile index 91814a00..00b00008 100644 --- a/Makefile +++ b/Makefile @@ -7,7 +7,7 @@ INCLUDES=-I lib -I common -I backend -I cfrontend # Files in lib/ -LIB=Coqlib.v Maps.v Sets.v union_find.v Lattice.v Ordered.v \ +LIB=Coqlib.v Maps.v Lattice.v Ordered.v \ Iteration.v Integers.v Floats.v Parmov.v # Files in common/ diff --git a/backend/Allocation.v b/backend/Allocation.v index c66d6b08..74c85cfe 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -3,6 +3,7 @@ Require Import Coqlib. Require Import Maps. +Require Import Lattice. Require Import AST. Require Import Integers. Require Import Values. @@ -100,7 +101,8 @@ Definition transfer general framework for backward dataflow analysis provided by module [Kildall]. *) -Module DS := Backward_Dataflow_Solver(Regset)(NodeSetBackward). +Module RegsetLat := LFSet(Regset). +Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward). Definition analyze (f: RTL.function): option (PMap.t Regset.t) := DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) nil. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 0b252d56..f0b2968f 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -2,6 +2,8 @@ RTL to LTL). *) Require Import Relations. +Require Import FSets. +Require Import SetoidList. Require Import Coqlib. Require Import Maps. Require Import AST. @@ -83,7 +85,7 @@ Lemma analyze_correct: f.(fn_code)!n <> None -> f.(fn_code)!s <> None -> In s (successors f n) -> - Regset.ge live!!n (transfer f s live!!s). + RegsetLat.ge live!!n (transfer f s live!!s). Proof. intros. eapply DS.fixpoint_solution. @@ -188,6 +190,7 @@ End REGALLOC_PROPERTIES. (** * Semantic agreement between RTL registers and LTL locations *) Require Import LTL. +Module RegsetP := Properties(Regset). Section AGREE. @@ -212,7 +215,7 @@ Hypothesis REGALLOC: regalloc f flive (live0 f flive) env = Some assign. of [assign r] can be arbitrary. *) Definition agree (live: Regset.t) (rs: regset) (ls: locset) : Prop := - forall (r: reg), Regset.mem r live = true -> ls (assign r) = rs#r. + forall (r: reg), Regset.In r live -> ls (assign r) = rs#r. (** What follows is a long list of lemmas expressing properties of the [agree_live_regs] predicate that are useful for the @@ -222,7 +225,7 @@ Definition agree (live: Regset.t) (rs: regset) (ls: locset) : Prop := Lemma agree_increasing: forall live1 live2 rs ls, - Regset.ge live1 live2 -> agree live1 rs ls -> + RegsetLat.ge live1 live2 -> agree live1 rs ls -> agree live2 rs ls. Proof. unfold agree; intros. @@ -231,14 +234,13 @@ Qed. (** Some useful special cases of [agree_increasing]. *) + Lemma agree_reg_live: forall r live rs ls, agree (reg_live r live) rs ls -> agree live rs ls. Proof. - intros. apply agree_increasing with (reg_live r live). - red; intros. case (Reg.eq r r0); intro. - subst r0. apply Regset.mem_add_same. - rewrite Regset.mem_add_other; auto. auto. + intros. apply agree_increasing with (reg_live r live); auto. + red. apply RegsetP.subset_add_2. apply RegsetP.subset_refl. Qed. Lemma agree_reg_list_live: @@ -266,7 +268,7 @@ Lemma agree_eval_reg: forall r live rs ls, agree (reg_live r live) rs ls -> ls (assign r) = rs#r. Proof. - intros. apply H. apply Regset.mem_add_same. + intros. apply H. apply Regset.add_1. auto. Qed. (** Same, for a list of registers. *) @@ -304,13 +306,13 @@ Qed. Lemma agree_assign_dead: forall live r rs ls v, - Regset.mem r live = false -> + ~Regset.In r live -> agree live rs ls -> agree live (rs#r <- v) ls. Proof. unfold agree; intros. case (Reg.eq r r0); intro. - subst r0. congruence. + subst r0. contradiction. rewrite Regmap.gso; auto. Qed. @@ -322,7 +324,7 @@ Qed. Lemma agree_assign_live: forall live r rs ls ls' v, (forall s, - Regset.mem s live = true -> s <> r -> assign s <> assign r) -> + Regset.In s live -> s <> r -> assign s <> assign r) -> ls' (assign r) = v -> (forall l, Loc.diff l (assign r) -> Loc.notin l temporaries -> ls' l = ls l) -> agree (reg_dead r live) rs ls -> @@ -332,8 +334,8 @@ Proof. case (Reg.eq r r0); intro. subst r0. rewrite Regmap.gss. assumption. rewrite Regmap.gso; auto. - rewrite H1. apply H2. rewrite Regset.mem_remove_other. auto. - auto. eapply regalloc_noteq_diff. eauto. apply H. auto. auto. + rewrite H1. apply H2. apply Regset.remove_2; auto. + eapply regalloc_noteq_diff. eauto. apply H. auto. auto. eapply regalloc_not_temporary; eauto. Qed. @@ -347,7 +349,7 @@ Qed. Lemma agree_move_live: forall live arg res rs (ls ls': locset), (forall r, - Regset.mem r live = true -> r <> res -> r <> arg -> + Regset.In r live -> r <> res -> r <> arg -> assign r <> assign res) -> ls' (assign res) = ls (assign arg) -> (forall l, Loc.diff l (assign res) -> Loc.notin l temporaries -> ls' l = ls l) -> @@ -357,17 +359,16 @@ Proof. unfold agree; intros. case (Reg.eq res r); intro. subst r. rewrite Regmap.gss. rewrite H0. apply H2. - apply Regset.mem_add_same. + apply Regset.add_1; auto. rewrite Regmap.gso; auto. case (Loc.eq (assign r) (assign res)); intro. rewrite e. rewrite H0. case (Reg.eq arg r); intro. - subst r. apply H2. apply Regset.mem_add_same. + subst r. apply H2. apply Regset.add_1; auto. elim (H r); auto. rewrite H1. apply H2. - case (Reg.eq arg r); intro. subst r. apply Regset.mem_add_same. - rewrite Regset.mem_add_other; auto. - rewrite Regset.mem_remove_other; auto. + case (Reg.eq arg r); intro. subst r. apply Regset.add_1; auto. + apply Regset.add_2. apply Regset.remove_2. auto. auto. eapply regalloc_noteq_diff; eauto. eapply regalloc_not_temporary; eauto. Qed. @@ -379,11 +380,10 @@ Qed. Lemma agree_call: forall live args ros res rs v (ls ls': locset), (forall r, - Regset.mem r live = true -> - r <> res -> + Regset.In r live -> r <> res -> ~(In (assign r) Conventions.destroyed_at_call)) -> (forall r, - Regset.mem r live = true -> r <> res -> assign r <> assign res) -> + Regset.In r live -> r <> res -> assign r <> assign res) -> ls' (assign res) = v -> (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> Loc.diff l (assign res) -> @@ -399,7 +399,7 @@ Proof. case (Reg.eq r res); intro. subst r. rewrite Regmap.gss. assumption. rewrite Regmap.gso; auto. rewrite H2. apply H4. - rewrite Regset.mem_remove_other; auto. + apply Regset.remove_2; auto. eapply regalloc_notin_notin; eauto. eapply regalloc_acceptable; eauto. eapply regalloc_noteq_diff; eauto. @@ -411,7 +411,7 @@ Qed. Lemma agree_init_regs: forall rl vl ls live, (forall r1 r2, - In r1 rl -> Regset.mem r2 live = true -> r1 <> r2 -> + In r1 rl -> Regset.In r2 live -> r1 <> r2 -> assign r1 <> assign r2) -> List.map ls (List.map assign rl) = vl -> agree (reg_list_dead rl live) (Regmap.init Vundef) ls -> @@ -421,15 +421,13 @@ Proof. assumption. destruct vl. discriminate. assert (agree (reg_dead a live) (init_regs vl rl) ls). - apply IHrl. intros. apply H. tauto. - case (Reg.eq a r2); intro. subst r2. - rewrite Regset.mem_remove_same in H3. discriminate. - rewrite Regset.mem_remove_other in H3; auto. + apply IHrl. intros. apply H. tauto. + eapply Regset.remove_3; eauto. auto. congruence. assumption. red; intros. case (Reg.eq a r); intro. subst r. rewrite Regmap.gss. congruence. - rewrite Regmap.gso; auto. apply H2. - rewrite Regset.mem_remove_other; auto. + rewrite Regmap.gso; auto. apply H2. + apply Regset.remove_2; auto. Qed. Lemma agree_parameters: @@ -437,7 +435,7 @@ Lemma agree_parameters: let params := f.(RTL.fn_params) in List.map ls (List.map assign params) = vl -> (forall r, - Regset.mem r (reg_list_dead params (live0 f flive)) = true -> + Regset.In r (reg_list_dead params (live0 f flive)) -> ls (assign r) = Vundef) -> agree (live0 f flive) (init_regs vl params) ls. Proof. @@ -1373,6 +1371,7 @@ Proof. intros; red; intros; CleanupHyps. caseEq (Regset.mem res live!!pc); intro LV; rewrite LV in AG. + generalize (Regset.mem_2 _ _ LV). intro LV'. assert (LL: (List.length (List.map assign args) <= 3)%nat). rewrite list_length_map. inversion WTI. simpl; omega. simpl; omega. @@ -1409,7 +1408,8 @@ Proof. exists ls. split. CleanupGoal. rewrite LV. apply exec_Bgoto; apply exec_refl. - apply agree_assign_dead; assumption. + apply agree_assign_dead; auto. + red; intro. exploit Regset.mem_1; eauto. congruence. Qed. Lemma transl_Iload_correct: @@ -1426,6 +1426,7 @@ Proof. caseEq (Regset.mem dst live!!pc); intro LV; rewrite LV in AG. (* dst is live *) + exploit Regset.mem_2; eauto. intro LV'. assert (LL: (List.length (List.map assign args) <= 2)%nat). rewrite list_length_map. inversion WTI. @@ -1453,6 +1454,7 @@ Proof. CleanupGoal. rewrite LV. apply exec_Bgoto; apply exec_refl. apply agree_assign_dead; auto. + red; intro; exploit Regset.mem_1; eauto. congruence. Qed. Lemma transl_Istore_correct: @@ -1681,16 +1683,15 @@ Qed. Remark regset_mem_reg_list_dead: forall rl r live, - Regset.mem r (reg_list_dead rl live) = true -> - ~(In r rl) /\ Regset.mem r live = true. + Regset.In r (reg_list_dead rl live) -> + ~(In r rl) /\ Regset.In r live. Proof. induction rl; simpl; intros. tauto. elim (IHrl r (reg_dead a live) H). intros. - assert (a <> r). red; intro; subst r. - rewrite Regset.mem_remove_same in H1. discriminate. - rewrite Regset.mem_remove_other in H1; auto. - tauto. + assert (a <> r). red; intro; subst r. + exploit Regset.remove_1; eauto. + intuition. eapply Regset.remove_3; eauto. Qed. Lemma transf_entrypoint_correct: @@ -1733,7 +1734,9 @@ Proof. intros [p [AP INP]]. clear INAP; subst ap. generalize (list_in_map_inv _ _ _ INAU). intros [u [AU INU]]. clear INAU; subst au. - generalize (Regset.elements_complete _ _ INU). intro. + assert (INU': InA Regset.E.eq u undefs). + rewrite InA_alt. exists u; intuition. + generalize (Regset.elements_2 _ _ INU'). intro. generalize (regset_mem_reg_list_dead _ _ _ H4). intros [A B]. eapply regalloc_noteq_diff; eauto. @@ -1761,7 +1764,11 @@ Proof. rewrite PARAMS1. assumption. fold oldentry; fold params. intros. apply UNDEFS1. apply in_map. - unfold undefs; apply Regset.elements_correct; auto. + unfold undefs. + change (transfer f oldentry live!!oldentry) + with (live0 f live). + exploit Regset.elements_1; eauto. + rewrite InA_alt. intros [r' [C D]]. hnf in C. subst r'. auto. Qed. Lemma transl_function_correct: diff --git a/backend/Coloring.v b/backend/Coloring.v index 0a2487cb..0b8a4ccc 100644 --- a/backend/Coloring.v +++ b/backend/Coloring.v @@ -81,8 +81,8 @@ Require Import InterfGraph. Definition add_interf_live (filter: reg -> bool) (res: reg) (live: Regset.t) (g: graph): graph := - Regset.fold - (fun g r => if filter r then add_interf r res g else g) live g. + Regset.fold graph + (fun r g => if filter r then add_interf r res g else g) live g. Definition add_interf_op (res: reg) (live: Regset.t) (g: graph): graph := @@ -101,7 +101,7 @@ Definition add_interf_move Definition add_interf_call (live: Regset.t) (destroyed: list mreg) (g: graph): graph := List.fold_left - (fun g mr => Regset.fold (fun g r => add_interf_mreg r mr g) live g) + (fun g mr => Regset.fold graph (fun r g => add_interf_mreg r mr g) live g) destroyed g. Fixpoint add_prefs_call diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v index 54d24cc4..f3801d07 100644 --- a/backend/Coloringproof.v +++ b/backend/Coloringproof.v @@ -1,5 +1,6 @@ (** Correctness of graph coloring. *) +Require Import SetoidList. Require Import Coqlib. Require Import Maps. Require Import AST. @@ -51,37 +52,36 @@ Lemma add_interf_live_incl: forall (filter: reg -> bool) res live g, graph_incl g (add_interf_live filter res live g). Proof. - intros. unfold add_interf_live. rewrite Regset.fold_spec. + intros. unfold add_interf_live. rewrite Regset.fold_1. apply add_interf_live_incl_aux. Qed. Lemma add_interf_live_correct_aux: - forall filter res live g r, - In r live -> filter r = true -> + forall filter res r live, + InA Regset.E.eq r live -> filter r = true -> + forall g, interfere r res (List.fold_left (fun g r => if filter r then add_interf r res g else g) live g). Proof. - induction live; simpl; intros. - contradiction. - elim H; intros. - subst a. rewrite H0. - generalize (add_interf_live_incl_aux filter res live (add_interf r res g)). + induction 1; simpl; intros. + hnf in H. subst y. rewrite H0. + generalize (add_interf_live_incl_aux filter res l (add_interf r res g)). intros [A B]. apply A. apply add_interf_correct. - apply IHlive; auto. + apply IHInA; auto. Qed. Lemma add_interf_live_correct: forall filter res live g r, - Regset.mem r live = true -> + Regset.In r live -> filter r = true -> interfere r res (add_interf_live filter res live g). Proof. - intros. unfold add_interf_live. rewrite Regset.fold_spec. + intros. unfold add_interf_live. rewrite Regset.fold_1. apply add_interf_live_correct_aux; auto. - apply Regset.elements_correct. auto. + apply Regset.elements_1. auto. Qed. Lemma add_interf_op_incl: @@ -93,15 +93,13 @@ Qed. Lemma add_interf_op_correct: forall res live g r, - Regset.mem r live = true -> + Regset.In r live -> r <> res -> interfere r res (add_interf_op res live g). Proof. intros. unfold add_interf_op. apply add_interf_live_correct. - auto. - case (Reg.eq r res); intro. - contradiction. auto. + auto. destruct (Reg.eq r res); congruence. Qed. Lemma add_interf_move_incl: @@ -113,18 +111,14 @@ Qed. Lemma add_interf_move_correct: forall arg res live g r, - Regset.mem r live = true -> + Regset.In r live -> r <> arg -> r <> res -> interfere r res (add_interf_move arg res live g). Proof. intros. unfold add_interf_move. apply add_interf_live_correct. - auto. - case (Reg.eq r res); intro. - contradiction. - case (Reg.eq r arg); intro. - contradiction. auto. + rewrite dec_eq_false; auto. rewrite dec_eq_false; auto. Qed. Lemma add_interf_call_incl_aux_1: @@ -142,9 +136,9 @@ Qed. Lemma add_interf_call_incl_aux_2: forall mr live g, graph_incl g - (Regset.fold (fun g r => add_interf_mreg r mr g) live g). + (Regset.fold graph (fun r g => add_interf_mreg r mr g) live g). Proof. - intros. rewrite Regset.fold_spec. apply add_interf_call_incl_aux_1. + intros. rewrite Regset.fold_1. apply add_interf_call_incl_aux_1. Qed. Lemma add_interf_call_incl: @@ -176,33 +170,32 @@ Proof. Qed. Lemma add_interf_call_correct_aux_1: - forall mr live g r, - In r live -> + forall mr r live, + InA Regset.E.eq r live -> + forall g, interfere_mreg r mr (List.fold_left (fun g r => add_interf_mreg r mr g) live g). Proof. - induction live; simpl; intros. - elim H. - elim H; intros. - subst a. eapply interfere_mreg_incl. + induction 1; simpl; intros. + hnf in H; subst y. eapply interfere_mreg_incl. apply add_interf_call_incl_aux_1. apply add_interf_mreg_correct. - apply IHlive; auto. + auto. Qed. Lemma add_interf_call_correct_aux_2: forall mr live g r, - Regset.mem r live = true -> + Regset.In r live -> interfere_mreg r mr - (Regset.fold (fun g r => add_interf_mreg r mr g) live g). + (Regset.fold graph (fun r g => add_interf_mreg r mr g) live g). Proof. - intros. rewrite Regset.fold_spec. apply add_interf_call_correct_aux_1. - apply Regset.elements_correct; auto. + intros. rewrite Regset.fold_1. apply add_interf_call_correct_aux_1. + apply Regset.elements_1. auto. Qed. Lemma add_interf_call_correct: forall live destroyed g r mr, - Regset.mem r live = true -> + Regset.In r live -> In mr destroyed -> interfere_mreg r mr (add_interf_call live destroyed g). Proof. @@ -240,7 +233,7 @@ Qed. Lemma add_interf_entry_correct: forall params live g r1 r2, In r1 params -> - Regset.mem r2 live = true -> + Regset.In r2 live -> r1 <> r2 -> interfere r1 r2 (add_interf_entry params live g). Proof. @@ -351,37 +344,37 @@ Definition correct_interf_instr match is_move_operation op args with | Some arg => forall r, - Regset.mem res live = true -> - Regset.mem r live = true -> + Regset.In res live -> + Regset.In r live -> r <> res -> r <> arg -> interfere r res g | None => forall r, - Regset.mem res live = true -> - Regset.mem r live = true -> + Regset.In res live -> + Regset.In r live -> r <> res -> interfere r res g end | Iload chunk addr args res s => forall r, - Regset.mem res live = true -> - Regset.mem r live = true -> + Regset.In res live -> + Regset.In r live -> r <> res -> interfere r res g | Icall sig ros args res s => (forall r mr, - Regset.mem r live = true -> + Regset.In r live -> In mr destroyed_at_call_regs -> r <> res -> interfere_mreg r mr g) /\ (forall r, - Regset.mem r live = true -> + Regset.In r live -> r <> res -> interfere r res g) | Ialloc arg res s => (forall r mr, - Regset.mem r live = true -> + Regset.In r live -> In mr destroyed_at_call_regs -> r <> res -> interfere_mreg r mr g) /\ (forall r, - Regset.mem r live = true -> + Regset.In r live -> r <> res -> interfere r res g) | _ => True @@ -414,11 +407,11 @@ Proof. intros. destruct instr; unfold add_edges_instr; unfold correct_interf_instr; auto. destruct (is_move_operation o l); intros. - rewrite H. eapply interfere_incl. + rewrite Regset.mem_1; auto. eapply interfere_incl. apply add_pref_incl. apply add_interf_move_correct; auto. - rewrite H. apply add_interf_op_correct; auto. + rewrite Regset.mem_1; auto. apply add_interf_op_correct; auto. - intros. rewrite H. apply add_interf_op_correct; auto. + intros. rewrite Regset.mem_1; auto. apply add_interf_op_correct; auto. split; intros. apply interfere_mreg_incl with @@ -427,7 +420,7 @@ Proof. eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. apply add_interf_op_incl. apply add_interf_call_correct; auto. - rewrite Regset.mem_remove_other; auto. + apply Regset.remove_2; auto. eapply interfere_incl. eapply graph_incl_trans; [idtac|apply add_prefs_call_incl]. @@ -441,7 +434,7 @@ Proof. eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. apply add_interf_op_incl. apply add_interf_call_correct; auto. - rewrite Regset.mem_remove_other; auto. + apply Regset.remove_2; auto. eapply interfere_incl. eapply graph_incl_trans; apply add_pref_mreg_incl. @@ -534,7 +527,7 @@ Qed. Lemma interf_graph_correct_3: forall f live live0 r1 r2, In r1 f.(fn_params) -> - Regset.mem r2 live0 = true -> + Regset.In r2 live0 -> r1 <> r2 -> interfere r1 r2 (interf_graph f live live0). Proof. @@ -617,8 +610,10 @@ Lemma check_coloring_3_correct: loc_acceptable (coloring r) /\ env r = Loc.type (coloring r). Proof. unfold check_coloring_3; intros. - generalize (Regset.for_all_spec _ H H0). intro. - elim (andb_prop _ _ H1); intros. + exploit Regset.for_all_2; eauto. + red; intros. hnf in H1. congruence. + apply Regset.mem_2. eauto. + simpl. intro. elim (andb_prop _ _ H1); intros. split. apply loc_is_acceptable_correct; auto. apply same_typ_correct; auto. Qed. @@ -649,7 +644,7 @@ Proof. elim (andb_prop _ _ H); intros. generalize (all_interf_regs_correct_1 _ _ _ H0). intros [A B]. - unfold allregs. rewrite A; rewrite B. + unfold allregs. rewrite Regset.mem_1; auto. rewrite Regset.mem_1; auto. eapply check_coloring_1_correct; eauto. Qed. @@ -663,7 +658,7 @@ Proof. elim (andb_prop _ _ H); intros. elim (andb_prop _ _ H2); intros. generalize (all_interf_regs_correct_2 _ _ _ H0). intros. - unfold allregs. rewrite H5. + unfold allregs. rewrite Regset.mem_1; auto. eapply check_coloring_2_correct; eauto. Qed. @@ -709,35 +704,35 @@ Definition correct_alloc_instr match is_move_operation op args with | Some arg => forall r, - Regset.mem res live!!pc = true -> - Regset.mem r live!!pc = true -> + Regset.In res live!!pc -> + Regset.In r live!!pc -> r <> res -> r <> arg -> alloc r <> alloc res | None => forall r, - Regset.mem res live!!pc = true -> - Regset.mem r live!!pc = true -> + Regset.In res live!!pc -> + Regset.In r live!!pc -> r <> res -> alloc r <> alloc res end | Iload chunk addr args res s => forall r, - Regset.mem res live!!pc = true -> - Regset.mem r live!!pc = true -> + Regset.In res live!!pc -> + Regset.In r live!!pc -> r <> res -> alloc r <> alloc res | Icall sig ros args res s => (forall r, - Regset.mem r live!!pc = true -> + Regset.In r live!!pc -> r <> res -> ~(In (alloc r) Conventions.destroyed_at_call)) /\ (forall r, - Regset.mem r live!!pc = true -> + Regset.In r live!!pc -> r <> res -> alloc r <> alloc res) | Ialloc arg res s => (forall r, - Regset.mem r live!!pc = true -> + Regset.In r live!!pc -> r <> res -> ~(In (alloc r) Conventions.destroyed_at_call)) /\ (forall r, - Regset.mem r live!!pc = true -> + Regset.In r live!!pc -> r <> res -> alloc r <> alloc res) | _ => True @@ -869,7 +864,7 @@ Lemma regalloc_correct_3: forall r1 r2, regalloc f live live0 env = Some alloc -> In r1 f.(fn_params) -> - Regset.mem r2 live0 = true -> + Regset.In r2 live0 -> r1 <> r2 -> alloc r1 <> alloc r2. Proof. diff --git a/backend/Constprop.v b/backend/Constprop.v index 330857cd..d34c6eed 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -36,7 +36,11 @@ Inductive approx : Set := Module Approx <: SEMILATTICE_WITH_TOP. Definition t := approx. - Lemma eq: forall (x y: t), {x=y} + {x<>y}. + Definition eq (x y: t) := (x = y). + Definition eq_refl: forall x, eq x x := (@refl_equal t). + Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). + Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). + Lemma eq_dec: forall (x y: t), {x=y} + {x<>y}. Proof. decide equality. apply Int.eq_dec. @@ -44,16 +48,25 @@ Module Approx <: SEMILATTICE_WITH_TOP. apply Int.eq_dec. apply ident_eq. Qed. + Definition beq (x y: t) := if eq_dec x y then true else false. + Lemma beq_correct: forall x y, beq x y = true -> x = y. + Proof. + unfold beq; intros. destruct (eq_dec x y). auto. congruence. + Qed. Definition ge (x y: t) : Prop := x = Unknown \/ y = Novalue \/ x = y. - Lemma ge_refl: forall x, ge x x. + Lemma ge_refl: forall x y, eq x y -> ge x y. Proof. - unfold ge; tauto. + unfold eq, ge; tauto. Qed. Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. Proof. unfold ge; intuition congruence. Qed. + Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. + Proof. + unfold eq, ge; intros; congruence. + Qed. Definition bot := Novalue. Definition top := Unknown. Lemma ge_bot: forall x, ge x bot. @@ -65,23 +78,23 @@ Module Approx <: SEMILATTICE_WITH_TOP. unfold ge, bot; tauto. Qed. Definition lub (x y: t) : t := - if eq x y then x else + if eq_dec x y then x else match x, y with | Novalue, _ => y | _, Novalue => x | _, _ => Unknown end. - Lemma lub_commut: forall x y, lub x y = lub y x. + Lemma lub_commut: forall x y, eq (lub x y) (lub y x). Proof. - unfold lub; intros. - case (eq x y); case (eq y x); intros; try congruence. + 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. - case (eq x y); intro. - apply ge_refl. + case (eq_dec x y); intro. + apply ge_refl. apply eq_refl. destruct x; destruct y; unfold ge; tauto. Qed. End Approx. diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v index 78112c33..5dc4fe9e 100644 --- a/backend/InterfGraph.v +++ b/backend/InterfGraph.v @@ -214,6 +214,7 @@ Definition all_interf_regs (g: graph) : Regset.t := g.(interf_reg_mreg) Regset.empty). +(* Lemma mem_add_tail: forall r r' u, Regset.mem r u = true -> Regset.mem r (Regset.add r' u) = true. @@ -222,28 +223,29 @@ Proof. subst r'. apply Regset.mem_add_same. rewrite Regset.mem_add_other; auto. Qed. - +*) Lemma in_setregreg_fold: forall g r1 r2 u, - SetRegReg.In (r1, r2) g \/ Regset.mem r1 u = true /\ Regset.mem r2 u = true -> - Regset.mem r1 (SetRegReg.fold _ add_intf2 g u) = true /\ - Regset.mem r2 (SetRegReg.fold _ add_intf2 g u) = true. + SetRegReg.In (r1, r2) g \/ Regset.In r1 u /\ Regset.In r2 u -> + Regset.In r1 (SetRegReg.fold _ add_intf2 g u) /\ + Regset.In r2 (SetRegReg.fold _ add_intf2 g u). Proof. set (add_intf2' := fun u r1r2 => add_intf2 r1r2 u). assert (forall l r1 r2 u, - InA OrderedRegReg.eq (r1,r2) l \/ Regset.mem r1 u = true /\ Regset.mem r2 u = true -> - Regset.mem r1 (List.fold_left add_intf2' l u) = true /\ - Regset.mem r2 (List.fold_left add_intf2' l u) = true). + InA OrderedRegReg.eq (r1,r2) l \/ Regset.In r1 u /\ Regset.In r2 u -> + Regset.In r1 (List.fold_left add_intf2' l u) /\ + Regset.In r2 (List.fold_left add_intf2' l u)). induction l; intros; simpl. elim H; intro. inversion H0. auto. apply IHl. destruct a as [a1 a2]. elim H; intro. inversion H0; subst. red in H2. simpl in H2. destruct H2. red in H1. red in H2. subst r1 r2. - right; unfold add_intf2', add_intf2; simpl; split. - apply Regset.mem_add_same. apply mem_add_tail. apply Regset.mem_add_same. + right; unfold add_intf2', add_intf2; simpl; split. + apply Regset.add_1. auto. + apply Regset.add_2. apply Regset.add_1. auto. tauto. right; unfold add_intf2', add_intf2; simpl; split; - apply mem_add_tail; apply mem_add_tail; tauto. + apply Regset.add_2; apply Regset.add_2; tauto. intros. rewrite SetRegReg.fold_1. apply H. intuition. left. apply SetRegReg.elements_1. auto. @@ -251,8 +253,8 @@ Qed. Lemma in_setregreg_fold': forall g r u, - Regset.mem r u = true -> - Regset.mem r (SetRegReg.fold _ add_intf2 g u) = true. + Regset.In r u -> + Regset.In r (SetRegReg.fold _ add_intf2 g u). Proof. intros. exploit in_setregreg_fold. eauto. intros [A B]. eauto. @@ -260,23 +262,23 @@ Qed. Lemma in_setregmreg_fold: forall g r1 mr2 u, - SetRegMreg.In (r1, mr2) g \/ Regset.mem r1 u = true -> - Regset.mem r1 (SetRegMreg.fold _ add_intf1 g u) = true. + SetRegMreg.In (r1, mr2) g \/ Regset.In r1 u -> + Regset.In r1 (SetRegMreg.fold _ add_intf1 g u). Proof. set (add_intf1' := fun u r1mr2 => add_intf1 r1mr2 u). assert (forall l r1 mr2 u, - InA OrderedRegMreg.eq (r1,mr2) l \/ Regset.mem r1 u = true -> - Regset.mem r1 (List.fold_left add_intf1' l u) = true). + InA OrderedRegMreg.eq (r1,mr2) l \/ Regset.In r1 u -> + Regset.In r1 (List.fold_left add_intf1' l u)). induction l; intros; simpl. elim H; intro. inversion H0. auto. apply IHl with mr2. destruct a as [a1 a2]. elim H; intro. inversion H0; subst. red in H2. simpl in H2. destruct H2. red in H1. red in H2. subst r1 mr2. right; unfold add_intf1', add_intf1; simpl. - apply Regset.mem_add_same. + apply Regset.add_1; auto. tauto. right; unfold add_intf1', add_intf1; simpl. - apply mem_add_tail; auto. + apply Regset.add_2; auto. intros. rewrite SetRegMreg.fold_1. apply H with mr2. intuition. left. apply SetRegMreg.elements_1. auto. @@ -285,8 +287,8 @@ Qed. Lemma all_interf_regs_correct_1: forall r1 r2 g, SetRegReg.In (r1, r2) g.(interf_reg_reg) -> - Regset.mem r1 (all_interf_regs g) = true /\ - Regset.mem r2 (all_interf_regs g) = true. + Regset.In r1 (all_interf_regs g) /\ + Regset.In r2 (all_interf_regs g). Proof. intros. unfold all_interf_regs. apply in_setregreg_fold. tauto. @@ -295,7 +297,7 @@ Qed. Lemma all_interf_regs_correct_2: forall r1 mr2 g, SetRegMreg.In (r1, mr2) g.(interf_reg_mreg) -> - Regset.mem r1 (all_interf_regs g) = true. + Regset.In r1 (all_interf_regs g). Proof. intros. unfold all_interf_regs. apply in_setregreg_fold'. eapply in_setregmreg_fold. eauto. diff --git a/backend/Kildall.v b/backend/Kildall.v index a04528e5..2a4b4bda 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -179,7 +179,7 @@ Definition start_state := Definition propagate_succ (s: state) (out: L.t) (n: positive) := let oldl := s.(st_in)!!n in let newl := L.lub oldl out in - if L.eq oldl newl + if L.beq oldl newl then s else mkstate (PMap.set n newl s.(st_in)) (NS.add n s.(st_wrk)). @@ -225,7 +225,7 @@ Definition in_incr (in1 in2: PMap.t L.t) : Prop := Lemma in_incr_refl: forall in1, in_incr in1 in1. Proof. - unfold in_incr; intros. apply L.ge_refl. + unfold in_incr; intros. apply L.ge_refl. apply L.eq_refl. Qed. Lemma in_incr_trans: @@ -239,11 +239,11 @@ Lemma propagate_succ_incr: in_incr st.(st_in) (propagate_succ st out n).(st_in). Proof. unfold in_incr, propagate_succ; simpl; intros. - case (L.eq st.(st_in)!!n (L.lub st.(st_in)!!n out)); intro. - apply L.ge_refl. + case (L.beq st.(st_in)!!n (L.lub st.(st_in)!!n out)). + apply L.ge_refl. apply L.eq_refl. simpl. case (peq n n0); intro. subst n0. rewrite PMap.gss. apply L.ge_lub_left. - rewrite PMap.gso; auto. apply L.ge_refl. + rewrite PMap.gso; auto. apply L.ge_refl. apply L.eq_refl. Qed. Lemma propagate_succ_list_incr: @@ -309,11 +309,18 @@ Lemma propagate_succ_charact: (forall s, n <> s -> st'.(st_in)!!s = st.(st_in)!!s). Proof. unfold propagate_succ; intros; simpl. - case (L.eq (st_in st) !! n (L.lub (st_in st) !! n out)); intro. - split. rewrite e. rewrite L.lub_commut. apply L.ge_lub_left. + predSpec L.beq L.beq_correct + ((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. auto. + simpl. split. - rewrite PMap.gss. rewrite L.lub_commut. apply L.ge_lub_left. + rewrite PMap.gss. + eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. + apply L.ge_lub_left. intros. rewrite PMap.gso; auto. Qed. @@ -344,7 +351,7 @@ Lemma propagate_succ_incr_worklist: NS.In x st.(st_wrk) -> NS.In x (propagate_succ st out n).(st_wrk). Proof. intros. unfold propagate_succ. - case (L.eq (st_in st) !! n (L.lub (st_in st) !! n out)); intro. + case (L.beq (st_in st) !! n (L.lub (st_in st) !! n out)). auto. simpl. rewrite NS.add_spec. auto. Qed. @@ -364,7 +371,7 @@ Lemma propagate_succ_records_changes: NS.In s st'.(st_wrk) \/ st'.(st_in)!!s = st.(st_in)!!s. Proof. simpl. intros. unfold propagate_succ. - case (L.eq (st_in st) !! n (L.lub (st_in st) !! n out)); intro. + case (L.beq (st_in st) !! n (L.lub (st_in st) !! n out)). right; auto. case (peq s n); intro. subst s. left. simpl. rewrite NS.add_spec. auto. @@ -465,7 +472,9 @@ Proof. induction ep; simpl; intros. elim H. elim H; intros. - subst a. rewrite PMap.gss. rewrite L.lub_commut. apply L.ge_lub_left. + subst a. rewrite PMap.gss. + eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. + apply L.ge_lub_left. 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. diff --git a/backend/Linearize.v b/backend/Linearize.v index 667b5d41..3151628c 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -3,7 +3,6 @@ Require Import Coqlib. Require Import Maps. -Require Import Sets. Require Import AST. Require Import Values. Require Import Globalenvs. diff --git a/backend/Registers.v b/backend/Registers.v index 5b1c7230..578e4b87 100644 --- a/backend/Registers.v +++ b/backend/Registers.v @@ -7,7 +7,9 @@ Require Import Coqlib. Require Import AST. Require Import Maps. -Require Import Sets. +Require Import Ordered. +Require Import FSets. +Require FSetAVL. Definition reg: Set := positive. @@ -45,4 +47,4 @@ Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level). (** Sets of registers *) -Module Regset := MakeSet(PTree). +Module Regset := FSetAVL.Make(OrderedPositive). diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 34a1080f..a3afae20 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -1,8 +1,10 @@ (** Translation from Csharpminor to Cminor. *) +Require Import FSets. +Require FSetAVL. Require Import Coqlib. Require Import Maps. -Require Import Sets. +Require Import Ordered. Require Import AST. Require Import Integers. Require Mem. @@ -287,7 +289,7 @@ Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt) (** Computation of the set of variables whose address is taken in a piece of Csharpminor code. *) -Module Identset := MakeSet(PTree). +Module Identset := FSetAVL.Make(OrderedPositive). Fixpoint addr_taken_expr (e: Csharpminor.expr): Identset.t := match e with diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 93eb99d9..ad31ff19 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -1,8 +1,8 @@ (** Correctness proof for Cminor generation. *) +Require Import FSets. Require Import Coqlib. Require Import Maps. -Require Import Sets. Require Import AST. Require Import Integers. Require Import Floats. diff --git a/extraction/.depend b/extraction/.depend index f320d0dd..53f84687 100644 --- a/extraction/.depend +++ b/extraction/.depend @@ -4,28 +4,28 @@ ../caml/Coloringaux.cmi: Registers.cmi RTLtyping.cmi RTL.cmi Locations.cmi \ InterfGraph.cmi ../caml/PrintPPC.cmi: PPC.cmi -../caml/Camlcoq.cmo: Integers.cmi Datatypes.cmi CList.cmi BinPos.cmi \ - BinInt.cmi -../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CList.cmx BinPos.cmx \ - BinInt.cmx -../caml/Cil2Csyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \ - CList.cmi AST.cmi -../caml/Cil2Csyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \ - CList.cmx AST.cmx ../caml/CMlexer.cmo: ../caml/Camlcoq.cmo ../caml/CMparser.cmi \ ../caml/CMlexer.cmi ../caml/CMlexer.cmx: ../caml/Camlcoq.cmx ../caml/CMparser.cmx \ ../caml/CMlexer.cmi -../caml/CMparser.cmo: Op.cmi Integers.cmi Int.cmi Datatypes.cmi Cminor.cmi \ +../caml/CMparser.cmo: Op.cmi Integers.cmi Datatypes.cmi Cminor.cmi \ Cmconstr.cmi ../caml/Camlcoq.cmo CList.cmi BinPos.cmi BinInt.cmi AST.cmi \ ../caml/CMparser.cmi -../caml/CMparser.cmx: Op.cmx Integers.cmx Int.cmx Datatypes.cmx Cminor.cmx \ +../caml/CMparser.cmx: Op.cmx Integers.cmx Datatypes.cmx Cminor.cmx \ Cmconstr.cmx ../caml/Camlcoq.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \ ../caml/CMparser.cmi ../caml/CMtypecheck.cmo: Op.cmi Integers.cmi Datatypes.cmi Cminor.cmi \ ../caml/Camlcoq.cmo CList.cmi AST.cmi ../caml/CMtypecheck.cmi ../caml/CMtypecheck.cmx: Op.cmx Integers.cmx Datatypes.cmx Cminor.cmx \ ../caml/Camlcoq.cmx CList.cmx AST.cmx ../caml/CMtypecheck.cmi +../caml/Camlcoq.cmo: Integers.cmi Datatypes.cmi CList.cmi BinPos.cmi \ + BinInt.cmi +../caml/Camlcoq.cmx: Integers.cmx Datatypes.cmx CList.cmx BinPos.cmx \ + BinInt.cmx +../caml/Cil2Csyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \ + CList.cmi AST.cmi +../caml/Cil2Csyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \ + CList.cmx AST.cmx ../caml/Coloringaux.cmo: Registers.cmi RTLtyping.cmi RTL.cmi Maps.cmi \ Locations.cmi InterfGraph.cmi Datatypes.cmi Conventions.cmi \ ../caml/Camlcoq.cmo BinPos.cmi BinInt.cmi AST.cmi ../caml/Coloringaux.cmi @@ -40,6 +40,10 @@ ../caml/Main2.cmx: ../caml/PrintPPC.cmx ../caml/PrintCsyntax.cmx Main.cmx \ Datatypes.cmx Csyntax.cmx ../caml/Cil2Csyntax.cmx ../caml/CMtypecheck.cmx \ ../caml/CMparser.cmx ../caml/CMlexer.cmx +../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \ + ../caml/Camlcoq.cmo CList.cmi AST.cmi +../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \ + ../caml/Camlcoq.cmx CList.cmx AST.cmx ../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \ CList.cmi AST.cmi ../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \ @@ -54,23 +58,26 @@ ../caml/Camlcoq.cmo CList.cmi AST.cmi ../caml/RTLtypingaux.cmx: Registers.cmx RTL.cmx Op.cmx Maps.cmx Datatypes.cmx \ ../caml/Camlcoq.cmx CList.cmx AST.cmx +AST.cmi: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ + CList.cmi BinPos.cmi BinInt.cmi Allocation.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi \ Parallelmove.cmi Op.cmi Maps.cmi Locations.cmi LTL.cmi Datatypes.cmi \ Conventions.cmi Coloring.cmi CList.cmi BinPos.cmi AST.cmi -AST.cmi: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi BinPos.cmi BinInt.cmi BinInt.cmi: Datatypes.cmi BinPos.cmi BinNat.cmi BinNat.cmi: Specif.cmi Datatypes.cmi BinPos.cmi BinPos.cmi: Peano.cmi Datatypes.cmi Bool.cmi: Specif.cmi Datatypes.cmi +CInt.cmi: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi CList.cmi: Specif.cmi Datatypes.cmi +CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \ + Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi Cmconstr.cmi: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \ Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi -Cminorgen.cmi: Zmax.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \ - Datatypes.cmi Csharpminor.cmi Coqlib.cmi Cminor.cmi Cmconstr.cmi \ - CList.cmi BinPos.cmi BinInt.cmi AST.cmi Cminor.cmi: Values.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ Datatypes.cmi CList.cmi BinInt.cmi AST.cmi +Cminorgen.cmi: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Mem.cmi \ + Maps.cmi Integers.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi Cminor.cmi \ + Cmconstr.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi AST.cmi Coloring.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \ Locations.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ CList.cmi BinInt.cmi AST.cmi @@ -81,8 +88,6 @@ Conventions.cmi: Locations.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \ BinInt.cmi AST.cmi Coqlib.cmi: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi Datatypes.cmi CList.cmi \ BinPos.cmi BinInt.cmi -CSE.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \ - Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi Csharpminor.cmi: Zmax.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \ AST.cmi @@ -92,37 +97,36 @@ Csyntax.cmi: Zmax.cmi Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi \ Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \ CList.cmi AST.cmi -Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi -FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi \ - Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi -FSetBridge.cmi: Specif.cmi FSetInterface.cmi Datatypes.cmi CList.cmi -FSetFacts.cmi: Specif.cmi setoid.cmi FSetInterface.cmi Datatypes.cmi +FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Datatypes.cmi \ + CList.cmi CInt.cmi BinPos.cmi BinInt.cmi +FSetFacts.cmi: Specif.cmi Setoid.cmi FSetInterface.cmi Datatypes.cmi FSetInterface.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi FSetList.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi +Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi Globalenvs.cmi: Values.cmi Mem.cmi Maps.cmi Integers.cmi Datatypes.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Integers.cmi: Zpower.cmi Zdiv.cmi Specif.cmi Datatypes.cmi Coqlib.cmi \ CList.cmi Bool.cmi BinPos.cmi BinInt.cmi InterfGraph.cmi: Specif.cmi Registers.cmi OrderedType.cmi Locations.cmi \ - Int.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi -Int.cmi: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi + Datatypes.cmi Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Iteration.cmi: Wf.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi -Kildall.cmi: Specif.cmi setoid.cmi OrderedType.cmi Maps.cmi Lattice.cmi \ - Iteration.cmi Int.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \ +Kildall.cmi: Specif.cmi Setoid.cmi OrderedType.cmi Maps.cmi Lattice.cmi \ + Iteration.cmi Datatypes.cmi Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi \ BinInt.cmi -Lattice.cmi: Specif.cmi Maps.cmi Datatypes.cmi BinPos.cmi -Linearize.cmi: Specif.cmi Op.cmi Maps.cmi Linear.cmi Lattice.cmi LTL.cmi \ - Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi +LTL.cmi: Values.cmi Specif.cmi Op.cmi Maps.cmi Locations.cmi Integers.cmi \ + Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi BinPos.cmi \ + BinInt.cmi AST.cmi +Lattice.cmi: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \ + BinPos.cmi Linear.cmi: Values.cmi Specif.cmi Op.cmi Locations.cmi Integers.cmi \ Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ AST.cmi +Linearize.cmi: Specif.cmi Op.cmi Maps.cmi Linear.cmi Lattice.cmi LTL.cmi \ + Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi Lineartyping.cmi: Zmax.cmi Locations.cmi Linear.cmi Datatypes.cmi \ Conventions.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Locations.cmi: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \ BinInt.cmi AST.cmi -LTL.cmi: Values.cmi Specif.cmi Op.cmi Maps.cmi Locations.cmi Integers.cmi \ - Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi BinPos.cmi \ - BinInt.cmi AST.cmi Mach.cmi: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Mem.cmi \ Locations.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi Coqlib.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi @@ -138,30 +142,28 @@ Op.cmi: Values.cmi Specif.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ Ordered.cmi: Specif.cmi OrderedType.cmi Maps.cmi Datatypes.cmi Coqlib.cmi \ BinPos.cmi OrderedType.cmi: Specif.cmi Datatypes.cmi +PPC.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ + Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi +PPCgen.cmi: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \ + Datatypes.cmi Coqlib.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi Parallelmove.cmi: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi Parmov.cmi: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi Peano.cmi: Datatypes.cmi -PPCgen.cmi: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \ - Datatypes.cmi Coqlib.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi -PPC.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \ - Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi -Registers.cmi: Specif.cmi Maps.cmi Datatypes.cmi Coqlib.cmi CList.cmi \ - BinPos.cmi AST.cmi -RTLgen.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \ - Datatypes.cmi Coqlib.cmi Cminor.cmi CList.cmi BinPos.cmi AST.cmi RTL.cmi: Values.cmi Registers.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi +RTLgen.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \ + Datatypes.cmi Coqlib.cmi Cminor.cmi CList.cmi BinPos.cmi AST.cmi RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \ Coqlib.cmi CList.cmi AST.cmi -setoid.cmi: Datatypes.cmi -Sets.cmi: Specif.cmi Maps.cmi Datatypes.cmi CList.cmi +Registers.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi Datatypes.cmi \ + Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi AST.cmi +Setoid.cmi: Datatypes.cmi Specif.cmi: Datatypes.cmi Stacking.cmi: Specif.cmi Op.cmi Mach.cmi Locations.cmi Lineartyping.cmi \ Linear.cmi Integers.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Sumbool.cmi: Specif.cmi Datatypes.cmi Tunneling.cmi: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi -union_find.cmi: Wf.cmi Specif.cmi Datatypes.cmi Values.cmi: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ BinPos.cmi BinInt.cmi AST.cmi ZArith_dec.cmi: Sumbool.cmi Specif.cmi Datatypes.cmi BinInt.cmi @@ -171,21 +173,20 @@ Zdiv.cmi: Zbool.cmi ZArith_dec.cmi Specif.cmi Datatypes.cmi BinPos.cmi \ BinInt.cmi Zeven.cmi: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zmax.cmi: Datatypes.cmi BinInt.cmi -Zmin.cmi: Datatypes.cmi BinInt.cmi Zmisc.cmi: Datatypes.cmi BinPos.cmi BinInt.cmi Zpower.cmi: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi -Allocation.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi \ - Parallelmove.cmi Op.cmi Maps.cmi Locations.cmi LTL.cmi Kildall.cmi \ - Datatypes.cmi Conventions.cmi Coloring.cmi CList.cmi BinPos.cmi AST.cmi \ - Allocation.cmi -Allocation.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx \ - Parallelmove.cmx Op.cmx Maps.cmx Locations.cmx LTL.cmx Kildall.cmx \ - Datatypes.cmx Conventions.cmx Coloring.cmx CList.cmx BinPos.cmx AST.cmx \ - Allocation.cmi AST.cmo: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi AST.cmx: Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx \ CList.cmx BinPos.cmx BinInt.cmx AST.cmi +Allocation.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi \ + Parallelmove.cmi Op.cmi Maps.cmi Locations.cmi Lattice.cmi LTL.cmi \ + Kildall.cmi Datatypes.cmi Conventions.cmi Coloring.cmi CList.cmi \ + BinPos.cmi AST.cmi Allocation.cmi +Allocation.cmx: Specif.cmx Registers.cmx RTLtyping.cmx RTL.cmx \ + Parallelmove.cmx Op.cmx Maps.cmx Locations.cmx Lattice.cmx LTL.cmx \ + Kildall.cmx Datatypes.cmx Conventions.cmx Coloring.cmx CList.cmx \ + BinPos.cmx AST.cmx Allocation.cmi BinInt.cmo: Datatypes.cmi BinPos.cmi BinNat.cmi BinInt.cmi BinInt.cmx: Datatypes.cmx BinPos.cmx BinNat.cmx BinInt.cmi BinNat.cmo: Specif.cmi Datatypes.cmi BinPos.cmi BinNat.cmi @@ -194,22 +195,32 @@ BinPos.cmo: Peano.cmi Datatypes.cmi BinPos.cmi BinPos.cmx: Peano.cmx Datatypes.cmx BinPos.cmi Bool.cmo: Specif.cmi Datatypes.cmi Bool.cmi Bool.cmx: Specif.cmx Datatypes.cmx Bool.cmi +CInt.cmo: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi CInt.cmi +CInt.cmx: Zmax.cmx ZArith_dec.cmx Specif.cmx BinPos.cmx BinInt.cmx CInt.cmi CList.cmo: Specif.cmi Datatypes.cmi CList.cmi CList.cmx: Specif.cmx Datatypes.cmx CList.cmi +CSE.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Kildall.cmi \ + Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \ + AST.cmi CSE.cmi +CSE.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx Kildall.cmx \ + Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \ + AST.cmx CSE.cmi Cmconstr.cmo: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \ Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Cmconstr.cmi Cmconstr.cmx: Specif.cmx Op.cmx Integers.cmx Datatypes.cmx Compare_dec.cmx \ Cminor.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx Cmconstr.cmi -Cminorgen.cmo: Zmax.cmi Specif.cmi Sets.cmi Op.cmi Mem.cmi Maps.cmi \ - Integers.cmi Datatypes.cmi Csharpminor.cmi Coqlib.cmi Cminor.cmi \ - Cmconstr.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Cminorgen.cmi -Cminorgen.cmx: Zmax.cmx Specif.cmx Sets.cmx Op.cmx Mem.cmx Maps.cmx \ - Integers.cmx Datatypes.cmx Csharpminor.cmx Coqlib.cmx Cminor.cmx \ - Cmconstr.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx Cminorgen.cmi Cminor.cmo: Values.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ Datatypes.cmi CList.cmi BinInt.cmi AST.cmi Cminor.cmi Cminor.cmx: Values.cmx Op.cmx Maps.cmx Integers.cmx Globalenvs.cmx \ Datatypes.cmx CList.cmx BinInt.cmx AST.cmx Cminor.cmi +Cminorgen.cmo: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Mem.cmi \ + Maps.cmi Integers.cmi FSetAVL.cmi Datatypes.cmi Csharpminor.cmi \ + Coqlib.cmi Cminor.cmi Cmconstr.cmi CList.cmi BinPos.cmi BinInt.cmi \ + AST.cmi Cminorgen.cmi +Cminorgen.cmx: Zmax.cmx Specif.cmx OrderedType.cmx Ordered.cmx Op.cmx Mem.cmx \ + Maps.cmx Integers.cmx FSetAVL.cmx Datatypes.cmx Csharpminor.cmx \ + Coqlib.cmx Cminor.cmx Cmconstr.cmx CList.cmx BinPos.cmx BinInt.cmx \ + AST.cmx Cminorgen.cmi Coloring.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \ Locations.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ ../caml/Coloringaux.cmi CList.cmi BinInt.cmi AST.cmi Coloring.cmi @@ -232,12 +243,6 @@ Coqlib.cmo: Zdiv.cmi ZArith_dec.cmi Wf.cmi Specif.cmi Datatypes.cmi CList.cmi \ BinPos.cmi BinInt.cmi Coqlib.cmi Coqlib.cmx: Zdiv.cmx ZArith_dec.cmx Wf.cmx Specif.cmx Datatypes.cmx CList.cmx \ BinPos.cmx BinInt.cmx Coqlib.cmi -CSE.cmo: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Kildall.cmi \ - Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \ - AST.cmi CSE.cmi -CSE.cmx: Specif.cmx Registers.cmx RTL.cmx Op.cmx Maps.cmx Kildall.cmx \ - Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \ - AST.cmx CSE.cmi Csharpminor.cmo: Zmax.cmi Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \ AST.cmi Csharpminor.cmi @@ -258,21 +263,13 @@ Ctyping.cmx: Specif.cmx Maps.cmx Datatypes.cmx Csyntax.cmx Coqlib.cmx \ CList.cmx AST.cmx Ctyping.cmi Datatypes.cmo: Datatypes.cmi Datatypes.cmx: Datatypes.cmi -Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \ - Floats.cmi -Floats.cmx: Specif.cmx Integers.cmx ../caml/Floataux.cmx Datatypes.cmx \ - Floats.cmi -FSetAVL.cmo: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi FSetList.cmi \ - Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi FSetAVL.cmi -FSetAVL.cmx: Wf.cmx Specif.cmx Peano.cmx OrderedType.cmx Int.cmx FSetList.cmx \ - Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx FSetAVL.cmi -FSetBridge.cmo: Specif.cmi FSetInterface.cmi Datatypes.cmi CList.cmi \ - FSetBridge.cmi -FSetBridge.cmx: Specif.cmx FSetInterface.cmx Datatypes.cmx CList.cmx \ - FSetBridge.cmi -FSetFacts.cmo: Specif.cmi setoid.cmi OrderedType.cmi FSetInterface.cmi \ +FSetAVL.cmo: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi FSetList.cmi \ + Datatypes.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi FSetAVL.cmi +FSetAVL.cmx: Wf.cmx Specif.cmx Peano.cmx OrderedType.cmx FSetList.cmx \ + Datatypes.cmx CList.cmx CInt.cmx BinPos.cmx BinInt.cmx FSetAVL.cmi +FSetFacts.cmo: Specif.cmi Setoid.cmi OrderedType.cmi FSetInterface.cmi \ Datatypes.cmi FSetFacts.cmi -FSetFacts.cmx: Specif.cmx setoid.cmx OrderedType.cmx FSetInterface.cmx \ +FSetFacts.cmx: Specif.cmx Setoid.cmx OrderedType.cmx FSetInterface.cmx \ Datatypes.cmx FSetFacts.cmi FSetInterface.cmo: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi \ FSetInterface.cmi @@ -280,6 +277,10 @@ FSetInterface.cmx: Specif.cmx OrderedType.cmx Datatypes.cmx CList.cmx \ FSetInterface.cmi FSetList.cmo: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi FSetList.cmi FSetList.cmx: Specif.cmx OrderedType.cmx Datatypes.cmx CList.cmx FSetList.cmi +Floats.cmo: Specif.cmi Integers.cmi ../caml/Floataux.cmo Datatypes.cmi \ + Floats.cmi +Floats.cmx: Specif.cmx Integers.cmx ../caml/Floataux.cmx Datatypes.cmx \ + Floats.cmi Globalenvs.cmo: Values.cmi Mem.cmi Maps.cmi Integers.cmi Datatypes.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Globalenvs.cmi Globalenvs.cmx: Values.cmx Mem.cmx Maps.cmx Integers.cmx Datatypes.cmx \ @@ -289,37 +290,43 @@ Integers.cmo: Zpower.cmi Zdiv.cmi Specif.cmi Datatypes.cmi Coqlib.cmi \ Integers.cmx: Zpower.cmx Zdiv.cmx Specif.cmx Datatypes.cmx Coqlib.cmx \ CList.cmx Bool.cmx BinPos.cmx BinInt.cmx Integers.cmi InterfGraph.cmo: Specif.cmi Registers.cmi OrderedType.cmi Ordered.cmi \ - Locations.cmi Int.cmi FSetAVL.cmi Datatypes.cmi Coqlib.cmi CList.cmi \ - BinPos.cmi BinInt.cmi InterfGraph.cmi + Locations.cmi FSetAVL.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi \ + BinInt.cmi InterfGraph.cmi InterfGraph.cmx: Specif.cmx Registers.cmx OrderedType.cmx Ordered.cmx \ - Locations.cmx Int.cmx FSetAVL.cmx Datatypes.cmx Coqlib.cmx CList.cmx \ - BinPos.cmx BinInt.cmx InterfGraph.cmi -Int.cmo: Zmax.cmi ZArith_dec.cmi Specif.cmi BinPos.cmi BinInt.cmi Int.cmi -Int.cmx: Zmax.cmx ZArith_dec.cmx Specif.cmx BinPos.cmx BinInt.cmx Int.cmi + Locations.cmx FSetAVL.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx \ + BinInt.cmx InterfGraph.cmi Iteration.cmo: Wf.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \ Iteration.cmi Iteration.cmx: Wf.cmx Specif.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \ Iteration.cmi -Kildall.cmo: Specif.cmi setoid.cmi OrderedType.cmi Maps.cmi Lattice.cmi \ - Iteration.cmi Int.cmi FSetFacts.cmi FSetAVL.cmi Datatypes.cmi Coqlib.cmi \ +Kildall.cmo: Specif.cmi Setoid.cmi OrderedType.cmi Maps.cmi Lattice.cmi \ + Iteration.cmi FSetFacts.cmi FSetAVL.cmi Datatypes.cmi Coqlib.cmi \ CList.cmi BinPos.cmi BinInt.cmi Kildall.cmi -Kildall.cmx: Specif.cmx setoid.cmx OrderedType.cmx Maps.cmx Lattice.cmx \ - Iteration.cmx Int.cmx FSetFacts.cmx FSetAVL.cmx Datatypes.cmx Coqlib.cmx \ +Kildall.cmx: Specif.cmx Setoid.cmx OrderedType.cmx Maps.cmx Lattice.cmx \ + Iteration.cmx FSetFacts.cmx FSetAVL.cmx Datatypes.cmx Coqlib.cmx \ CList.cmx BinPos.cmx BinInt.cmx Kildall.cmi -Lattice.cmo: Specif.cmi Maps.cmi Datatypes.cmi BinPos.cmi Lattice.cmi -Lattice.cmx: Specif.cmx Maps.cmx Datatypes.cmx BinPos.cmx Lattice.cmi -Linearize.cmo: Specif.cmi Op.cmi Maps.cmi Linear.cmi Lattice.cmi LTL.cmi \ - Kildall.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi \ - Linearize.cmi -Linearize.cmx: Specif.cmx Op.cmx Maps.cmx Linear.cmx Lattice.cmx LTL.cmx \ - Kildall.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx AST.cmx \ - Linearize.cmi +LTL.cmo: Values.cmi Specif.cmi Op.cmi Maps.cmi Locations.cmi Integers.cmi \ + Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi BinPos.cmi \ + BinInt.cmi AST.cmi LTL.cmi +LTL.cmx: Values.cmx Specif.cmx Op.cmx Maps.cmx Locations.cmx Integers.cmx \ + Globalenvs.cmx Datatypes.cmx Conventions.cmx CList.cmx BinPos.cmx \ + BinInt.cmx AST.cmx LTL.cmi +Lattice.cmo: Specif.cmi Maps.cmi FSetInterface.cmi Datatypes.cmi Bool.cmi \ + BinPos.cmi Lattice.cmi +Lattice.cmx: Specif.cmx Maps.cmx FSetInterface.cmx Datatypes.cmx Bool.cmx \ + BinPos.cmx Lattice.cmi Linear.cmo: Values.cmi Specif.cmi Op.cmi Locations.cmi Integers.cmi \ Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ AST.cmi Linear.cmi Linear.cmx: Values.cmx Specif.cmx Op.cmx Locations.cmx Integers.cmx \ Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \ AST.cmx Linear.cmi +Linearize.cmo: Specif.cmi Op.cmi Maps.cmi Linear.cmi Lattice.cmi LTL.cmi \ + Kildall.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi AST.cmi \ + Linearize.cmi +Linearize.cmx: Specif.cmx Op.cmx Maps.cmx Linear.cmx Lattice.cmx LTL.cmx \ + Kildall.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx AST.cmx \ + Linearize.cmi Lineartyping.cmo: Zmax.cmi Locations.cmi Linear.cmi Datatypes.cmi \ Conventions.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi Lineartyping.cmi Lineartyping.cmx: Zmax.cmx Locations.cmx Linear.cmx Datatypes.cmx \ @@ -330,12 +337,6 @@ Locations.cmx: Values.cmx Specif.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \ BinInt.cmx AST.cmx Locations.cmi Logic.cmo: Logic.cmi Logic.cmx: Logic.cmi -LTL.cmo: Values.cmi Specif.cmi Op.cmi Maps.cmi Locations.cmi Integers.cmi \ - Globalenvs.cmi Datatypes.cmi Conventions.cmi CList.cmi BinPos.cmi \ - BinInt.cmi AST.cmi LTL.cmi -LTL.cmx: Values.cmx Specif.cmx Op.cmx Maps.cmx Locations.cmx Integers.cmx \ - Globalenvs.cmx Datatypes.cmx Conventions.cmx CList.cmx BinPos.cmx \ - BinInt.cmx AST.cmx LTL.cmi Mach.cmo: Zmax.cmi Zdiv.cmi Values.cmi Specif.cmi Op.cmi Mem.cmi Maps.cmi \ Locations.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi Coqlib.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Mach.cmi @@ -368,6 +369,18 @@ Ordered.cmx: Specif.cmx OrderedType.cmx Maps.cmx Datatypes.cmx Coqlib.cmx \ BinPos.cmx Ordered.cmi OrderedType.cmo: Specif.cmi Datatypes.cmi OrderedType.cmi OrderedType.cmx: Specif.cmx Datatypes.cmx OrderedType.cmi +PPC.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ + Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ + AST.cmi PPC.cmi +PPC.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx Globalenvs.cmx \ + Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \ + AST.cmx PPC.cmi +PPCgen.cmo: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \ + Datatypes.cmi Coqlib.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi \ + PPCgen.cmi +PPCgen.cmx: Specif.cmx PPC.cmx Op.cmx Mach.cmx Locations.cmx Integers.cmx \ + Datatypes.cmx Coqlib.cmx CList.cmx Bool.cmx BinPos.cmx BinInt.cmx AST.cmx \ + PPCgen.cmi Parallelmove.cmo: Parmov.cmi Locations.cmi Datatypes.cmi CList.cmi AST.cmi \ Parallelmove.cmi Parallelmove.cmx: Parmov.cmx Locations.cmx Datatypes.cmx CList.cmx AST.cmx \ @@ -376,40 +389,28 @@ Parmov.cmo: Specif.cmi Peano.cmi Datatypes.cmi CList.cmi Parmov.cmi Parmov.cmx: Specif.cmx Peano.cmx Datatypes.cmx CList.cmx Parmov.cmi Peano.cmo: Datatypes.cmi Peano.cmi Peano.cmx: Datatypes.cmx Peano.cmi -PPCgen.cmo: Specif.cmi PPC.cmi Op.cmi Mach.cmi Locations.cmi Integers.cmi \ - Datatypes.cmi Coqlib.cmi CList.cmi Bool.cmi BinPos.cmi BinInt.cmi AST.cmi \ - PPCgen.cmi -PPCgen.cmx: Specif.cmx PPC.cmx Op.cmx Mach.cmx Locations.cmx Integers.cmx \ - Datatypes.cmx Coqlib.cmx CList.cmx Bool.cmx BinPos.cmx BinInt.cmx AST.cmx \ - PPCgen.cmi -PPC.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ - Floats.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ - AST.cmi PPC.cmi -PPC.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx Globalenvs.cmx \ - Floats.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \ - AST.cmx PPC.cmi -Registers.cmo: Specif.cmi Sets.cmi Maps.cmi Datatypes.cmi Coqlib.cmi \ - CList.cmi BinPos.cmi AST.cmi Registers.cmi -Registers.cmx: Specif.cmx Sets.cmx Maps.cmx Datatypes.cmx Coqlib.cmx \ - CList.cmx BinPos.cmx AST.cmx Registers.cmi +RTL.cmo: Values.cmi Registers.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ + Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi RTL.cmi +RTL.cmx: Values.cmx Registers.cmx Op.cmx Maps.cmx Integers.cmx Globalenvs.cmx \ + Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx RTL.cmi RTLgen.cmo: Specif.cmi Registers.cmi ../caml/RTLgenaux.cmo RTL.cmi Op.cmi \ Maps.cmi Integers.cmi Datatypes.cmi Coqlib.cmi Cminor.cmi CList.cmi \ BinPos.cmi AST.cmi RTLgen.cmi RTLgen.cmx: Specif.cmx Registers.cmx ../caml/RTLgenaux.cmx RTL.cmx Op.cmx \ Maps.cmx Integers.cmx Datatypes.cmx Coqlib.cmx Cminor.cmx CList.cmx \ BinPos.cmx AST.cmx RTLgen.cmi -RTL.cmo: Values.cmi Registers.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ - Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi RTL.cmi -RTL.cmx: Values.cmx Registers.cmx Op.cmx Maps.cmx Integers.cmx Globalenvs.cmx \ - Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx RTL.cmi RTLtyping.cmo: Specif.cmi Registers.cmi ../caml/RTLtypingaux.cmo RTL.cmi \ Op.cmi Maps.cmi Datatypes.cmi Coqlib.cmi CList.cmi AST.cmi RTLtyping.cmi RTLtyping.cmx: Specif.cmx Registers.cmx ../caml/RTLtypingaux.cmx RTL.cmx \ Op.cmx Maps.cmx Datatypes.cmx Coqlib.cmx CList.cmx AST.cmx RTLtyping.cmi -setoid.cmo: Datatypes.cmi setoid.cmi -setoid.cmx: Datatypes.cmx setoid.cmi -Sets.cmo: Specif.cmi Maps.cmi Datatypes.cmi CList.cmi Sets.cmi -Sets.cmx: Specif.cmx Maps.cmx Datatypes.cmx CList.cmx Sets.cmi +Registers.cmo: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi FSetAVL.cmi \ + Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \ + Registers.cmi +Registers.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Maps.cmx FSetAVL.cmx \ + Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \ + Registers.cmi +Setoid.cmo: Datatypes.cmi Setoid.cmi +Setoid.cmx: Datatypes.cmx Setoid.cmi Specif.cmo: Datatypes.cmi Specif.cmi Specif.cmx: Datatypes.cmx Specif.cmi Stacking.cmo: Specif.cmi Op.cmi Mach.cmi Locations.cmi Lineartyping.cmi \ @@ -422,8 +423,6 @@ Sumbool.cmo: Specif.cmi Datatypes.cmi Sumbool.cmi Sumbool.cmx: Specif.cmx Datatypes.cmx Sumbool.cmi Tunneling.cmo: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi Tunneling.cmi Tunneling.cmx: Maps.cmx LTL.cmx Datatypes.cmx AST.cmx Tunneling.cmi -union_find.cmo: Wf.cmi Specif.cmi Datatypes.cmi union_find.cmi -union_find.cmx: Wf.cmx Specif.cmx Datatypes.cmx union_find.cmi Values.cmo: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ BinPos.cmi BinInt.cmi AST.cmi Values.cmi Values.cmx: Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx \ @@ -446,8 +445,6 @@ Zeven.cmo: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zeven.cmi Zeven.cmx: Specif.cmx Datatypes.cmx BinPos.cmx BinInt.cmx Zeven.cmi Zmax.cmo: Datatypes.cmi BinInt.cmi Zmax.cmi Zmax.cmx: Datatypes.cmx BinInt.cmx Zmax.cmi -Zmin.cmo: Datatypes.cmi BinInt.cmi Zmin.cmi -Zmin.cmx: Datatypes.cmx BinInt.cmx Zmin.cmi Zmisc.cmo: Datatypes.cmi BinPos.cmi BinInt.cmi Zmisc.cmi Zmisc.cmx: Datatypes.cmx BinPos.cmx BinInt.cmx Zmisc.cmi Zpower.cmo: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zpower.cmi diff --git a/extraction/Makefile b/extraction/Makefile index 0df787b6..69b5f572 100644 --- a/extraction/Makefile +++ b/extraction/Makefile @@ -1,9 +1,10 @@ FILES=\ Datatypes.ml Logic.ml Wf.ml Peano.ml Specif.ml Compare_dec.ml \ - Bool.ml CList.ml Sumbool.ml BinPos.ml BinNat.ml BinInt.ml \ + Bool.ml CList.ml Sumbool.ml Setoid.ml BinPos.ml BinNat.ml BinInt.ml \ ZArith_dec.ml Zeven.ml Zmax.ml Zmisc.ml Zbool.ml Zpower.ml Zdiv.ml \ - Int.ml OrderedType.ml FSetInterface.ml FSetFacts.ml FSetList.ml FSetAVL.ml \ - Coqlib.ml Maps.ml Sets.ml AST.ml Iteration.ml Integers.ml \ + OrderedType.ml FSetInterface.ml FSetFacts.ml FSetList.ml \ + CInt.ml FSetAVL.ml \ + Coqlib.ml Maps.ml Ordered.ml AST.ml Iteration.ml Integers.ml \ ../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Parmov.ml Values.ml \ Mem.ml Globalenvs.ml \ Csyntax.ml Ctyping.ml Csharpminor.ml Cshmgen.ml \ @@ -16,7 +17,7 @@ FILES=\ Lattice.ml Kildall.ml \ Constprop.ml CSE.ml \ LTL.ml \ - Ordered.ml InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \ + InterfGraph.ml ../caml/Coloringaux.ml Coloring.ml \ Parallelmove.ml Allocation.ml \ Tunneling.ml Linear.ml Lineartyping.ml Linearize.ml \ Mach.ml Stacking.ml \ @@ -30,7 +31,7 @@ FILES=\ EXTRACTEDFILES:=$(filter-out ../caml/%, $(FILES)) GENFILES:=$(EXTRACTEDFILES) $(EXTRACTEDFILES:.ml=.mli) -CAMLINCL=-I ../caml -I ../cil/obj/x86_LINUX +CAMLINCL=-I ../caml -I ../cil/obj/x86_LINUX -I ../cil/obj/ppc_DARWIN OCAMLC=ocamlc -g $(CAMLINCL) OCAMLOPT=ocamlopt $(CAMLINCL) OCAMLDEP=ocamldep $(CAMLINCL) @@ -57,12 +58,14 @@ extraction: @echo "Fixing file names..." @mv list.ml CList.ml @mv list.mli CList.mli + @mv int.ml CInt.ml + @mv int.mli CInt.mli @for i in $(GENFILES); do \ j=`./uncapitalize $$i`; \ test -f $$i || (test -f $$j && mv $$j $$i); \ done - @echo "Conversion List -> CList..." - @perl -p -i -e 's/\bList\b/CList/g;' $(GENFILES) + @echo "Conversion List -> CList and Int -> CInt..." + @./convert $(GENFILES) @echo "Patching files..." @for i in *.patch; do patch < $$i; done diff --git a/extraction/convert b/extraction/convert new file mode 100755 index 00000000..a29178a1 --- /dev/null +++ b/extraction/convert @@ -0,0 +1,8 @@ +#!/usr/bin/perl -pi + +s/\bList\b/CList/g; +s/\bInt\.Z_as_Int\b/CInt.Z_as_Int/g; +s/\bInt\.Int\b/CInt.Int/g; +s/\bInt\.MoreInt\b/CInt.MoreInt/g; +s/^open Int$//; + diff --git a/lib/Lattice.v b/lib/Lattice.v index 7adcffba..7ef1b9e1 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -2,6 +2,7 @@ Require Import Coqlib. Require Import Maps. +Require Import FSets. (** * Signatures of semi-lattices *) @@ -13,14 +14,20 @@ Require Import Maps. Module Type SEMILATTICE. Variable t: Set. - Variable eq: forall (x y: t), {x=y} + {x<>y}. + Variable eq: t -> t -> Prop. + Hypothesis eq_refl: forall x, eq x x. + Hypothesis eq_sym: forall x y, eq x y -> eq y x. + Hypothesis eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Variable beq: t -> t -> bool. + Hypothesis beq_correct: forall x y, beq x y = true -> eq x y. Variable ge: t -> t -> Prop. - Hypothesis ge_refl: forall x, ge x x. + Hypothesis ge_refl: forall x y, eq x y -> ge x y. Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Hypothesis ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. Variable bot: t. Hypothesis ge_bot: forall x, ge x bot. Variable lub: t -> t -> t. - Hypothesis lub_commut: forall x y, lub x y = lub y x. + Hypothesis lub_commut: forall x y, eq (lub x y) (lub y x). Hypothesis ge_lub_left: forall x y, ge (lub x y) x. End SEMILATTICE. @@ -31,16 +38,22 @@ End SEMILATTICE. Module Type SEMILATTICE_WITH_TOP. Variable t: Set. - Variable eq: forall (x y: t), {x=y} + {x<>y}. + Variable eq: t -> t -> Prop. + Hypothesis eq_refl: forall x, eq x x. + Hypothesis eq_sym: forall x y, eq x y -> eq y x. + Hypothesis eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Variable beq: t -> t -> bool. + Hypothesis beq_correct: forall x y, beq x y = true -> eq x y. Variable ge: t -> t -> Prop. - Hypothesis ge_refl: forall x, ge x x. + Hypothesis ge_refl: forall x y, eq x y -> ge x y. Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Hypothesis ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. Variable bot: t. Hypothesis ge_bot: forall x, ge x bot. Variable top: t. Hypothesis ge_top: forall x, ge top x. Variable lub: t -> t -> t. - Hypothesis lub_commut: forall x y, lub x y = lub y x. + Hypothesis lub_commut: forall x y, eq (lub x y) (lub y x). Hypothesis ge_lub_left: forall x y, ge (lub x y) x. End SEMILATTICE_WITH_TOP. @@ -59,13 +72,6 @@ Inductive t_ : Set := Definition t: Set := t_. -Lemma eq: forall (x y: t), {x=y} + {x<>y}. -Proof. - assert (forall m1 m2: PTree.t L.t, {m1=m2} + {m1<>m2}). - apply PTree.eq. exact L.eq. - decide equality. -Qed. - Definition get (p: positive) (x: t) : L.t := match x with | Bot_except m => @@ -96,12 +102,48 @@ Proof. intros. destruct x; simpl; rewrite PTree.gso; auto. Qed. +Definition eq (x y: t) : Prop := + forall p, L.eq (get p x) (get p y). + +Lemma eq_refl: forall x, eq x x. +Proof. + unfold eq; intros. apply L.eq_refl. +Qed. + +Lemma eq_sym: forall x y, eq x y -> eq y x. +Proof. + unfold eq; intros. apply L.eq_sym; auto. +Qed. + +Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. +Proof. + unfold eq; intros. eapply L.eq_trans; eauto. +Qed. + +Definition beq (x y: t) : bool := + match x, y with + | Bot_except m, Bot_except n => PTree.beq L.beq m n + | Top_except m, Top_except n => PTree.beq L.beq m n + | _, _ => false + end. + +Lemma beq_correct: forall x y, beq x y = true -> eq x y. +Proof. + destruct x; destruct y; simpl; intro; try congruence. + red; intro; simpl. + generalize (PTree.beq_correct L.eq L.beq L.beq_correct t0 t1 H p). + destruct (t0!p); destruct (t1!p); intuition. apply L.eq_refl. + red; intro; simpl. + generalize (PTree.beq_correct L.eq L.beq L.beq_correct t0 t1 H p). + destruct (t0!p); destruct (t1!p); intuition. apply L.eq_refl. +Qed. + Definition ge (x y: t) : Prop := forall p, L.ge (get p x) (get p y). -Lemma ge_refl: forall x, ge x x. +Lemma ge_refl: forall x y, eq x y -> ge x y. Proof. - unfold ge; intros. apply L.ge_refl. + unfold ge, eq; intros. apply L.ge_refl. auto. Qed. Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. @@ -109,6 +151,11 @@ Proof. unfold ge; intros. apply L.ge_trans with (get p y); auto. Qed. +Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. +Proof. + unfold eq,ge; intros. eapply L.ge_compat; eauto. +Qed. + Definition bot := Bot_except (PTree.empty L.t). Lemma get_bot: forall p, get p bot = L.bot. @@ -177,11 +224,13 @@ Definition lub (x y: t) : t := end. Lemma lub_commut: - forall x y, lub x y = lub y x. + forall x y, eq (lub x y) (lub y x). Proof. - destruct x; destruct y; unfold lub; decEq; - apply PTree.combine_commut; intros; - (destruct i; destruct j; auto; decEq; apply L.lub_commut). + intros x y p. + destruct x; destruct y; simpl; + repeat rewrite PTree.gcombine; auto; + destruct t0!p; destruct t1!p; + try apply L.eq_refl; try apply L.lub_commut. Qed. Lemma ge_lub_left: @@ -191,7 +240,8 @@ Proof. rewrite PTree.gcombine. destruct t0!p. destruct t1!p. apply L.ge_lub_left. - apply L.ge_refl. destruct t1!p. apply L.ge_bot. apply L.ge_refl. + apply L.ge_refl. apply L.eq_refl. + destruct t1!p. apply L.ge_bot. apply L.ge_refl. apply L.eq_refl. auto. rewrite PTree.gcombine. @@ -201,16 +251,67 @@ Proof. rewrite PTree.gcombine. destruct t0!p. destruct t1!p. apply L.ge_lub_left. - apply L.ge_refl. apply L.ge_refl. auto. + apply L.ge_refl. apply L.eq_refl. apply L.ge_refl. apply L.eq_refl. auto. rewrite PTree.gcombine. destruct t0!p. destruct t1!p. apply L.ge_lub_left. - apply L.ge_top. apply L.ge_refl. + apply L.ge_top. apply L.ge_refl. apply L.eq_refl. auto. Qed. End LPMap. +(** * Semi-lattice over a set. *) + +(** Given a set [S: FSetInterface.S], the following functor + implements a semi-lattice over these sets, ordered by inclusion. *) + +Module LFSet (S: FSetInterface.S) <: SEMILATTICE. + + Definition t := S.t. + + Definition eq (x y: t) := S.Equal x y. + Definition eq_refl: forall x, eq x x := S.eq_refl. + Definition eq_sym: forall x y, eq x y -> eq y x := S.eq_sym. + Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := S.eq_trans. + Definition beq: t -> t -> bool := S.equal. + Definition beq_correct: forall x y, beq x y = true -> eq x y := S.equal_2. + + Definition ge (x y: t) := S.Subset y x. + Lemma ge_refl: forall x y, eq x y -> ge x y. + Proof. + unfold eq, ge, S.Equal, S.Subset; intros. firstorder. + Qed. + Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Proof. + unfold ge, S.Subset; intros. eauto. + Qed. + Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. + Proof. + unfold ge, eq, S.Subset, S.Equal; intros. firstorder. + Qed. + + Definition bot: t := S.empty. + Lemma ge_bot: forall x, ge x bot. + Proof. + unfold ge, bot, S.Subset; intros. elim (S.empty_1 H). + Qed. + + Definition lub: t -> t -> t := S.union. + Lemma lub_commut: forall x y, eq (lub x y) (lub y x). + Proof. + unfold lub, eq, S.Equal; intros. split; intro. + destruct (S.union_1 H). apply S.union_3; auto. apply S.union_2; auto. + destruct (S.union_1 H). apply S.union_3; auto. apply S.union_2; auto. + Qed. + + Lemma ge_lub_left: forall x y, ge (lub x y) x. + Proof. + unfold lub, ge, S.Subset; intros. apply S.union_2; auto. + Qed. + +End LFSet. + (** * Flat semi-lattice *) (** Given a type with decidable equality [X], the following functor @@ -227,9 +328,23 @@ Inductive t_ : Set := Definition t : Set := t_. -Lemma eq: forall (x y: t), {x=y} + {x<>y}. +Definition eq (x y: t) := (x = y). +Definition eq_refl: forall x, eq x x := (@refl_equal t). +Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). +Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). + +Definition beq (x y: t) : bool := + match x, y with + | Bot, Bot => true + | Inj u, Inj v => if X.eq u v then true else false + | Top, Top => true + | _, _ => false + end. + +Lemma beq_correct: forall x y, beq x y = true -> eq x y. Proof. - decide equality. apply X.eq. + unfold eq; destruct x; destruct y; simpl; try congruence; intro. + destruct (X.eq t0 t1); congruence. Qed. Definition ge (x y: t) : Prop := @@ -240,9 +355,9 @@ Definition ge (x y: t) : Prop := | _, _ => False end. -Lemma ge_refl: forall x, ge x x. +Lemma ge_refl: forall x y, eq x y -> ge x y. Proof. - unfold ge; destruct x; auto. + unfold eq, ge; intros; subst y; destruct x; auto. Qed. Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. @@ -251,6 +366,11 @@ Proof. transitivity t1; auto. Qed. +Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. +Proof. + unfold eq; intros; congruence. +Qed. + Definition bot: t := Bot. Lemma ge_bot: forall x, ge x bot. @@ -274,9 +394,9 @@ Definition lub (x y: t) : t := | Inj a, Inj b => if X.eq a b then Inj a else Top end. -Lemma lub_commut: forall x y, lub x y = lub y x. +Lemma lub_commut: forall x y, eq (lub x y) (lub y x). Proof. - destruct x; destruct y; simpl; auto. + unfold eq; destruct x; destruct y; simpl; auto. case (X.eq t0 t1); case (X.eq t1 t0); intros; congruence. Qed. @@ -297,17 +417,29 @@ Module LBoolean <: SEMILATTICE_WITH_TOP. Definition t := bool. -Lemma eq: forall (x y: t), {x=y} + {x<>y}. -Proof. decide equality. Qed. +Definition eq (x y: t) := (x = y). +Definition eq_refl: forall x, eq x x := (@refl_equal t). +Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). +Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). + +Definition beq : t -> t -> bool := eqb. + +Lemma beq_correct: forall x y, beq x y = true -> eq x y. +Proof eqb_prop. Definition ge (x y: t) : Prop := x = y \/ x = true. -Lemma ge_refl: forall x, ge x x. +Lemma ge_refl: forall x y, eq x y -> ge x y. Proof. unfold ge; tauto. Qed. Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. Proof. unfold ge; intuition congruence. Qed. +Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. +Proof. + unfold eq; intros; congruence. +Qed. + Definition bot := false. Lemma ge_bot: forall x, ge x bot. @@ -320,8 +452,8 @@ Proof. unfold ge, top; tauto. Qed. Definition lub (x y: t) := x || y. -Lemma lub_commut: forall x y, lub x y = lub y x. -Proof. intros; unfold lub. apply orb_comm. Qed. +Lemma lub_commut: forall x y, eq (lub x y) (lub y x). +Proof. intros; unfold eq, lub. apply orb_comm. Qed. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. destruct x; destruct y; compute; tauto. Qed. @@ -329,3 +461,4 @@ Proof. destruct x; destruct y; compute; tauto. Qed. End LBoolean. + diff --git a/lib/Maps.v b/lib/Maps.v index 22d9a370..238009b2 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -60,6 +60,19 @@ Module Type TREE. forall (A: Set) (i j: elt) (m: t A), i <> j -> get i (remove j m) = get i m. + (** Extensional equality between trees. *) + Variable beq: forall (A: Set), (A -> A -> bool) -> t A -> t A -> bool. + Hypothesis beq_correct: + forall (A: Set) (P: A -> A -> Prop) (cmp: A -> A -> bool), + (forall (x y: A), cmp x y = true -> P x y) -> + forall (t1 t2: t A), beq cmp t1 t2 = true -> + forall (x: elt), + match get x t1, get x t2 with + | None, None => True + | Some y1, Some y2 => P y1 y2 + | _, _ => False + end. + (** Applying a function to all data of a tree. *) Variable map: forall (A B: Set), (elt -> A -> B) -> t A -> t B. @@ -305,6 +318,75 @@ Module PTree <: TREE. auto. Qed. + Section EXTENSIONAL_EQUALITY. + + Variable A: Set. + Variable eqA: A -> A -> Prop. + Variable beqA: A -> A -> bool. + Hypothesis beqA_correct: forall x y, beqA x y = true -> eqA x y. + + Definition exteq (m1 m2: t A) : Prop := + forall (x: elt), + match get x m1, get x m2 with + | None, None => True + | Some y1, Some y2 => eqA y1 y2 + | _, _ => False + end. + + Fixpoint bempty (m: t A) : bool := + match m with + | Leaf => true + | Node l None r => bempty l && bempty r + | Node l (Some _) r => false + end. + + Lemma bempty_correct: + forall m, bempty m = true -> forall x, get x m = None. + Proof. + induction m; simpl; intros. + change (@Leaf A) with (empty A). apply gempty. + destruct o. congruence. destruct (andb_prop _ _ H). + destruct x; simpl; auto. + Qed. + + Fixpoint beq (m1 m2: t A) {struct m1} : bool := + match m1, m2 with + | Leaf, _ => bempty m2 + | _, Leaf => bempty m1 + | Node l1 o1 r1, Node l2 o2 r2 => + match o1, o2 with + | None, None => true + | Some y1, Some y2 => beqA y1 y2 + | _, _ => false + end + && beq l1 l2 && beq r1 r2 + end. + + Lemma beq_correct: + forall m1 m2, beq m1 m2 = true -> exteq m1 m2. + Proof. + induction m1; destruct m2; simpl. + intros; red; intros. change (@Leaf A) with (empty A). + repeat rewrite gempty. auto. + destruct o; intro. congruence. + red; intros. change (@Leaf A) with (empty A). rewrite gempty. + rewrite bempty_correct. auto. assumption. + destruct o; intro. congruence. + red; intros. change (@Leaf A) with (empty A). rewrite gempty. + rewrite bempty_correct. auto. assumption. + destruct o; destruct o0; simpl; intro; try congruence. + destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). + red; intros. destruct x; simpl. + apply IHm1_2; auto. apply IHm1_1; auto. + apply beqA_correct; auto. + destruct (andb_prop _ _ H). + red; intros. destruct x; simpl. + apply IHm1_2; auto. apply IHm1_1; auto. + auto. + Qed. + + End EXTENSIONAL_EQUALITY. + Fixpoint append (i j : positive) {struct i} : positive := match i with | xH => j diff --git a/lib/Sets.v b/lib/Sets.v deleted file mode 100644 index 0a809fcd..00000000 --- a/lib/Sets.v +++ /dev/null @@ -1,189 +0,0 @@ -(** Finite sets. This module implements finite sets over any type - that is equipped with a tree (partial finite mapping) structure. - The set structure forms a semi-lattice, ordered by set inclusion. - - It would have been better to use the [FSet] library, which provides - sets over any totally ordered type. However, there are technical - mismatches between the [FSet] export signature and our signature for - semi-lattices. For now, we keep this somewhat redundant - implementation of sets. -*) - -Require Import Coqlib. -Require Import Maps. -Require Import Lattice. - -Set Implicit Arguments. - -Module MakeSet (P: TREE) <: SEMILATTICE. - -(** Sets of elements of type [P.elt] are implemented as a partial mapping - from [P.elt] to the one-element type [unit]. *) - - Definition elt := P.elt. - - Definition t := P.t unit. - - Lemma eq: forall (a b: t), {a=b} + {a<>b}. - Proof. - unfold t; intros. apply P.eq. - intros. left. destruct x; destruct y; auto. - Qed. - - Definition empty := P.empty unit. - - Definition mem (r: elt) (s: t) := - match P.get r s with None => false | Some _ => true end. - - Definition add (r: elt) (s: t) := P.set r tt s. - - Definition remove (r: elt) (s: t) := P.remove r s. - - Definition union (s1 s2: t) := - P.combine - (fun e1 e2 => - match e1, e2 with - | None, None => None - | _, _ => Some tt - end) - s1 s2. - - Lemma mem_empty: - forall r, mem r empty = false. - Proof. - intro; unfold mem, empty. rewrite P.gempty. auto. - Qed. - - Lemma mem_add_same: - forall r s, mem r (add r s) = true. - Proof. - intros; unfold mem, add. rewrite P.gss. auto. - Qed. - - Lemma mem_add_other: - forall r r' s, r <> r' -> mem r' (add r s) = mem r' s. - Proof. - intros; unfold mem, add. rewrite P.gso; auto. - Qed. - - Lemma mem_remove_same: - forall r s, mem r (remove r s) = false. - Proof. - intros; unfold mem, remove. rewrite P.grs; auto. - Qed. - - Lemma mem_remove_other: - forall r r' s, r <> r' -> mem r' (remove r s) = mem r' s. - Proof. - intros; unfold mem, remove. rewrite P.gro; auto. - Qed. - - Lemma mem_union: - forall r s1 s2, mem r (union s1 s2) = (mem r s1 || mem r s2). - Proof. - intros; unfold union, mem. rewrite P.gcombine. - case (P.get r s1); case (P.get r s2); auto. - auto. - Qed. - - Definition elements (s: t) := - List.map (@fst elt unit) (P.elements s). - - Lemma elements_correct: - forall r s, mem r s = true -> In r (elements s). - Proof. - intros until s. unfold mem, elements. caseEq (P.get r s). - intros. change r with (fst (r, u)). apply in_map. - apply P.elements_correct. auto. - intros; discriminate. - Qed. - - Lemma elements_complete: - forall r s, In r (elements s) -> mem r s = true. - Proof. - unfold mem, elements. intros. - generalize (list_in_map_inv _ _ _ H). - intros [p [EQ IN]]. - destruct p. simpl in EQ. subst r. - rewrite (P.elements_complete _ _ _ IN). auto. - Qed. - - Definition fold (A: Set) (f: A -> elt -> A) (s: t) (x: A) := - P.fold (fun (x: A) (r: elt) (z: unit) => f x r) s x. - - Lemma fold_spec: - forall (A: Set) (f: A -> elt -> A) (s: t) (x: A), - fold f s x = List.fold_left f (elements s) x. - Proof. - intros. unfold fold. rewrite P.fold_spec. - unfold elements. generalize x; generalize (P.elements s). - induction l; simpl; auto. - Qed. - - Definition for_all (f: elt -> bool) (s: t) := - fold (fun b x => andb b (f x)) s true. - - Lemma for_all_spec: - forall f s x, - for_all f s = true -> mem x s = true -> f x = true. - Proof. - intros until x. unfold for_all. rewrite fold_spec. - assert (forall l b0, - fold_left (fun (b : bool) (x : elt) => b && f x) l b0 = true -> - b0 = true). - induction l; simpl; intros. - auto. - generalize (IHl _ H). intro. - elim (andb_prop _ _ H0); intros. auto. - assert (forall l, - fold_left (fun (b : bool) (x : elt) => b && f x) l true = true -> - In x l -> f x = true). - induction l; simpl; intros. - elim H1. - generalize (H _ _ H0); intro. - elim H1; intros. - subst x. auto. - apply IHl. rewrite H2 in H0; auto. auto. - intros. eapply H0; eauto. - apply elements_correct. auto. - Qed. - - Definition ge (s1 s2: t) : Prop := - forall r, mem r s2 = true -> mem r s1 = true. - - Lemma ge_refl: forall x, ge x x. - Proof. - unfold ge; intros. auto. - Qed. - - Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Proof. - unfold ge; intros. auto. - Qed. - - Definition bot := empty. - Definition lub := union. - - Lemma ge_bot: forall (x:t), ge x bot. - Proof. - unfold ge; intros. rewrite mem_empty in H. discriminate. - Qed. - - Lemma lub_commut: forall (x y: t), lub x y = lub y x. - Proof. - intros. unfold lub; unfold union. apply P.combine_commut. - intros; case i; case j; auto. - Qed. - - Lemma ge_lub_left: forall (x y: t), ge (lub x y) x. - Proof. - unfold ge, lub; intros. - rewrite mem_union. rewrite H. reflexivity. - Qed. - - Lemma ge_lub_right: forall (x y: t), ge (lub x y) y. - Proof. - intros. rewrite lub_commut. apply ge_lub_left. - Qed. - -End MakeSet. diff --git a/lib/union_find.v b/lib/union_find.v deleted file mode 100644 index 452459fa..00000000 --- a/lib/union_find.v +++ /dev/null @@ -1,484 +0,0 @@ -(** A purely functional union-find algorithm *) - -Require Import Wf. -Require Recdef. - -(** The ``union-find'' algorithm is used to represent equivalence classes - over a given type. It maintains a data structure representing a partition - of the type into equivalence classes. Three operations are provided: -- [empty], which returns the finest partition: each element of the type - is equivalent to itself only. -- [repr part x] returns a canonical representative for the equivalence - class of element [x] in partition [part]. Two elements [x] and [y] - are in the same equivalence class if and only if - [repr part x = repr part y]. -- [identify part x y] returns a new partition where the equivalence - classes of [x] and [y] are merged, and all equivalences valid in [part] - are still valid. - - The partitions are represented by partial mappings from elements - to elements. If [part] maps [x] to [y], this means that [x] and [y] - are in the same equivalence class. The canonical representative - of the class of [x] is obtained by iteratively following these mappings - until an element not mapped to anything is reached; this element is the - canonical representative, as returned by [repr]. - - In algorithm textbooks, the mapping is maintained imperatively by - storing pointers within elements. Here, we give a purely functional - presentation where the mapping is a separate functional data structure. -*) - -(** The elements of equivalence classes are represented by the following - signature: a type with a decidable equality. *) - -Module Type ELEMENT. - Variable T: Set. - Variable eq: forall (a b: T), {a = b} + {a <> b}. -End ELEMENT. - -(** The mapping structure over elements is represented by the following - signature. *) - -Module Type MAP. - Variable elt: Set. - Variable T: Set. - Variable empty: T. - Variable get: elt -> T -> option elt. - Variable add: elt -> elt -> T -> T. - - Hypothesis get_empty: forall (x: elt), get x empty = None. - Hypothesis get_add_1: - forall (x y: elt) (m: T), get x (add x y m) = Some y. - Hypothesis get_add_2: - forall (x y z: elt) (m: T), z <> x -> get z (add x y m) = get z m. -End MAP. - -(** Our implementation of union-find is a functor, parameterized by - a structure for elements and a structure for maps. It returns a - module with the following structure. *) - -Module Type UNIONFIND. - Variable elt: Set. - (** The type of partitions. *) - Variable T: Set. - - (** The operations over partitions. *) - Variable empty: T. - Variable repr: T -> elt -> elt. - Variable identify: T -> elt -> elt -> T. - - (** The relation implied by the partition [m]. *) - Definition sameclass (m: T) (x y: elt) : Prop := repr m x = repr m y. - - (* [sameclass] is an equivalence relation *) - Hypothesis sameclass_refl: - forall (m: T) (x: elt), sameclass m x x. - Hypothesis sameclass_sym: - forall (m: T) (x y: elt), sameclass m x y -> sameclass m y x. - Hypothesis sameclass_trans: - forall (m: T) (x y z: elt), - sameclass m x y -> sameclass m y z -> sameclass m x z. - - (* [repr m x] is a canonical representative of the equivalence class - of [x] in partition [m]. *) - Hypothesis repr_repr: - forall (m: T) (x: elt), repr m (repr m x) = repr m x. - Hypothesis sameclass_repr: - forall (m: T) (x: elt), sameclass m x (repr m x). - - (* [empty] is the finest partition *) - Hypothesis repr_empty: - forall (x: elt), repr empty x = x. - Hypothesis sameclass_empty: - forall (x y: elt), sameclass empty x y -> x = y. - - (* [identify] preserves existing equivalences and adds an equivalence - between the two elements provided. *) - Hypothesis sameclass_identify_1: - forall (m: T) (x y: elt), sameclass (identify m x y) x y. - Hypothesis sameclass_identify_2: - forall (m: T) (x y u v: elt), - sameclass m u v -> sameclass (identify m x y) u v. - -End UNIONFIND. - -(** Implementation of the union-find algorithm. *) - -Module Unionfind (E: ELEMENT) (M: MAP with Definition elt := E.T) - <: UNIONFIND with Definition elt := E.T. - -Definition elt := E.T. - -(* A set of equivalence classes over [elt] is represented by a map [m]. -- [M.get a m = Some a'] means that [a] is in the same class as [a']. -- [M.get a m = None] means that [a] is the canonical representative - for its equivalence class. -*) - -(** Such a map induces an ordering over type [elt]: - [repr_order m a a'] if and only if [M.get a' m = Some a]. - This ordering must be well founded (no cycles). *) - -Definition repr_order (m: M.T) (a a': elt) : Prop := - M.get a' m = Some a. - -(** The canonical representative of an element. - Needs Noetherian recursion. *) - -Section REPR. - -Variable m: M.T. -Variable wf: well_founded (repr_order m). - -Function repr_aux (a: elt) {wf (repr_order m) a} : elt := - match M.get a m with - | Some a' => repr_aux a' - | None => a - end. -Proof. - intros. assumption. - assumption. -Qed. - -Lemma repr_aux_none: - forall (a: elt), - M.get a m = None -> - repr_aux a = a. -Proof. - intros. rewrite repr_aux_equation. rewrite H. auto. -Qed. - -Lemma repr_aux_some: - forall (a a': elt), - M.get a m = Some a' -> - repr_aux a = repr_aux a'. -Proof. - intros. rewrite repr_aux_equation. rewrite H. auto. -Qed. - -Lemma repr_aux_canon: - forall (a: elt), M.get (repr_aux a) m = None. -Proof. - intros a0. - apply (repr_aux_ind (fun a a' => M.get a' m = None)). - auto. auto. -Qed. - -End REPR. - -(** The empty partition (each element in its own class) is well founded. *) - -Lemma wf_empty: - well_founded (repr_order M.empty). -Proof. - red. intro. apply Acc_intro. - intros b RO. - red in RO. - rewrite M.get_empty in RO. - discriminate. -Qed. - -(** Merging two equivalence classes. *) - -Section IDENTIFY. - -Variable m: M.T. -Hypothesis mwf: well_founded (repr_order m). -Variable a b: elt. -Hypothesis a_diff_b: a <> b. -Hypothesis a_canon: M.get a m = None. -Hypothesis b_canon: M.get b m = None. - -(** Identifying two distinct canonical representatives [a] and [b] - is achieved by mapping one to the other. *) - -Definition identify_base: M.T := M.add a b m. - -Lemma identify_base_b_canon: - M.get b identify_base = None. -Proof. - unfold identify_base. - rewrite M.get_add_2. - auto. - apply sym_not_eq. auto. -Qed. - -Lemma identify_base_a_maps_to_b: - M.get a identify_base = Some b. -Proof. - unfold identify_base. rewrite M.get_add_1. auto. -Qed. - -Lemma identify_base_repr_order: - forall (x y: elt), - repr_order identify_base x y -> - repr_order m x y \/ (y = a /\ x = b). -Proof. - intros x y. unfold identify_base. - unfold repr_order. - case (E.eq a y); intro. - rewrite e. rewrite M.get_add_1. - intro. injection H. intro. rewrite H0. tauto. - rewrite M.get_add_2; auto. -Qed. - -(** [identify_base] preserves well foundation. *) - -Lemma identify_base_order_wf: - well_founded (repr_order identify_base). -Proof. - red. - cut (forall (x: elt), Acc (repr_order m) x -> Acc (repr_order identify_base) x). - intro CUT. intro x. apply CUT. apply mwf. - - induction 1. - apply Acc_intro. intros. - destruct (identify_base_repr_order y x H1) as [A | [A B]]. - apply H0; auto. - subst x y. apply Acc_intro. intros z H4. - red in H4. rewrite identify_base_b_canon in H4. discriminate. -Qed. - -Lemma identify_aux_decomp: - forall (x: elt), - (M.get x m = None /\ M.get x identify_base = None) - \/ (x = a /\ M.get x m = None /\ M.get x identify_base = Some b) - \/ (exists y, M.get x m = Some y /\ M.get x identify_base = Some y). -Proof. - intro x. - unfold identify_base. - case (E.eq a x); intro. - rewrite <- e. rewrite M.get_add_1. - tauto. - rewrite M.get_add_2; auto. - case (M.get x m); intros. - right; right; exists e; tauto. - tauto. -Qed. - -Lemma identify_base_repr: - forall (x: elt), - repr_aux identify_base identify_base_order_wf x = - (if E.eq (repr_aux m mwf x) a then b else repr_aux m mwf x). -Proof. - apply (well_founded_ind mwf - (fun (x: elt) => - repr_aux identify_base identify_base_order_wf x = - (if E.eq (repr_aux m mwf x) a then b else repr_aux m mwf x))); - intros. - destruct (identify_aux_decomp x) as [[A B] | [[A [B C]] | [y [A B]]]]. - - rewrite (repr_aux_none identify_base); auto. - rewrite (repr_aux_none m mwf x); auto. - case (E.eq x a); intro. - subst x. - rewrite identify_base_a_maps_to_b in B. discriminate. - auto. - - subst x. rewrite (repr_aux_none m mwf a); auto. - case (E.eq a a); intro. - rewrite (repr_aux_some identify_base identify_base_order_wf a b); auto. - rewrite (repr_aux_none identify_base identify_base_order_wf b); auto. - apply identify_base_b_canon. - tauto. - - rewrite (repr_aux_some identify_base identify_base_order_wf x y); auto. - rewrite (repr_aux_some m mwf x y); auto. -Qed. - -Lemma identify_base_sameclass_1: - forall (x y: elt), - repr_aux m mwf x = repr_aux m mwf y -> - repr_aux identify_base identify_base_order_wf x = - repr_aux identify_base identify_base_order_wf y. -Proof. - intros. - rewrite identify_base_repr. - rewrite identify_base_repr. - rewrite H. - auto. -Qed. - -Lemma identify_base_sameclass_2: - forall (x y: elt), - repr_aux m mwf x = a -> - repr_aux m mwf y = b -> - repr_aux identify_base identify_base_order_wf x = - repr_aux identify_base identify_base_order_wf y. -Proof. - intros. - rewrite identify_base_repr. - rewrite identify_base_repr. - rewrite H. - case (E.eq a a); intro. - case (E.eq (repr_aux m mwf y) a); auto. - tauto. -Qed. - -End IDENTIFY. - -(** The union-find data structure is a record encapsulating a mapping - and a proof of well foundation. *) - -Record unionfind : Set := mkunionfind - { map: M.T; wf: well_founded (repr_order map) }. - -Definition T := unionfind. - -Definition repr (uf: unionfind) (a: elt) : elt := - repr_aux (map uf) (wf uf) a. - -Lemma repr_repr: - forall (uf: unionfind) (a: elt), repr uf (repr uf a) = repr uf a. -Proof. - intros. - unfold repr. - rewrite (repr_aux_none (map uf) (wf uf) (repr_aux (map uf) (wf uf) a)). - auto. - apply repr_aux_canon. -Qed. - -Definition empty := mkunionfind M.empty wf_empty. - -(** [identify] computes canonical representatives for the two elements - and adds a mapping from one to the other, unless they are already - equal. *) - -Definition identify (uf: unionfind) (a b: elt) : unionfind := - match E.eq (repr uf a) (repr uf b) with - | left EQ => - uf - | right NOTEQ => - mkunionfind - (identify_base (map uf) (repr uf a) (repr uf b)) - (identify_base_order_wf (map uf) (wf uf) - (repr uf a) (repr uf b) - NOTEQ - (repr_aux_canon (map uf) (wf uf) b)) - end. - -Definition sameclass (uf: unionfind) (a b: elt) : Prop := - repr uf a = repr uf b. - -Lemma sameclass_refl: - forall (uf: unionfind) (a: elt), sameclass uf a a. -Proof. - intros. red. auto. -Qed. - -Lemma sameclass_sym: - forall (uf: unionfind) (a b: elt), sameclass uf a b -> sameclass uf b a. -Proof. - intros. red. symmetry. exact H. -Qed. - -Lemma sameclass_trans: - forall (uf: unionfind) (a b c: elt), - sameclass uf a b -> sameclass uf b c -> sameclass uf a c. -Proof. - intros. red. transitivity (repr uf b). exact H. exact H0. -Qed. - -Lemma sameclass_repr: - forall (uf: unionfind) (a: elt), sameclass uf a (repr uf a). -Proof. - intros. red. symmetry. rewrite repr_repr. auto. -Qed. - -Lemma repr_empty: - forall (a: elt), repr empty a = a. -Proof. - intro a. unfold repr; unfold empty. - simpl. - apply repr_aux_none. - apply M.get_empty. -Qed. - -Lemma sameclass_empty: - forall (a b: elt), sameclass empty a b -> a = b. -Proof. - intros. red in H. rewrite repr_empty in H. - rewrite repr_empty in H. auto. -Qed. - -Lemma sameclass_identify_2: - forall (uf: unionfind) (a b x y: elt), - sameclass uf x y -> sameclass (identify uf a b) x y. -Proof. - intros. - unfold identify. - case (E.eq (repr uf a) (repr uf b)). - intro. auto. - intros; red; unfold repr; simpl. - apply identify_base_sameclass_1. - apply repr_aux_canon. - exact H. -Qed. - -Lemma sameclass_identify_1: - forall (uf: unionfind) (a b: elt), - sameclass (identify uf a b) a b. -Proof. - intros. - unfold identify. - case (E.eq (repr uf a) (repr uf b)). - intro. auto. - intros. - red; unfold repr; simpl. - apply identify_base_sameclass_2. - apply repr_aux_canon. - auto. - auto. -Qed. - -End Unionfind. - -(* Example of use 1: with association lists *) - -(* - -Require Import List. - -Module AListMap(E: ELEMENT) : MAP. - -Definition elt := E.T. -Definition T := list (elt * elt). -Definition empty : T := nil. -Fixpoint get (x: elt) (m: T) {struct m} : option elt := - match m with - | nil => None - | (a,b) :: t => - match E.eq x a with - | left _ => Some b - | right _ => get x t - end - end. -Definition add (x y: elt) (m: T) := (x,y) :: m. - -Lemma get_empty: forall (x: elt), get x empty = None. -Proof. - intro. unfold empty. simpl. auto. -Qed. - -Lemma get_add_1: - forall (x y: elt) (m: T), get x (add x y m) = Some y. -Proof. - intros. unfold add. simpl. - case (E.eq x x); intro. - auto. - tauto. -Qed. - -Lemma get_add_2: - forall (x y z: elt) (m: T), z <> x -> get z (add x y m) = get z m. -Proof. - intros. unfold add. simpl. - case (E.eq z x); intro. - subst z; tauto. - auto. -Qed. - -End AListMap. - -*) - diff --git a/test/c/Makefile b/test/c/Makefile index 16fead48..88969342 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -50,6 +50,11 @@ time_gcc: echo -n "$$i: "; $(TIME) ./$$i.gcc; \ done +time_compcert: + @for i in $(PROGS); do \ + echo -n "$$i: "; $(TIME) ./$$i.compcert; \ + done + clean: rm -f *.compcert *.gcc rm -f *.light.c *.s *.o *~ -- cgit