aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend12
-rw-r--r--Makefile2
-rw-r--r--backend/Allocation.v4
-rw-r--r--backend/Allocproof.v87
-rw-r--r--backend/Coloring.v6
-rw-r--r--backend/Coloringproof.v131
-rw-r--r--backend/Constprop.v31
-rw-r--r--backend/InterfGraph.v44
-rw-r--r--backend/Kildall.v31
-rw-r--r--backend/Linearize.v1
-rw-r--r--backend/Registers.v6
-rw-r--r--cfrontend/Cminorgen.v6
-rw-r--r--cfrontend/Cminorgenproof.v2
-rw-r--r--extraction/.depend257
-rw-r--r--extraction/Makefile17
-rwxr-xr-xextraction/convert8
-rw-r--r--lib/Lattice.v199
-rw-r--r--lib/Maps.v82
-rw-r--r--lib/Sets.v189
-rw-r--r--lib/union_find.v484
-rw-r--r--test/c/Makefile5
21 files changed, 594 insertions, 1010 deletions
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 *~
generated by cgit (git 2.34.1) at 2024-06-02 15:25:32 +0000