Merge of branch value-analysis.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 615 insertions, 53 deletions

diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 929b61e..ca48341 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -363,6 +363,16 @@ let time3 name fn arg1 arg2 arg3 =
     add_to_timer name (Unix.gettimeofday() -. start);
     raise x
 
+let time4 name fn arg1 arg2 arg3 arg4 =
+  let start = Unix.gettimeofday() in
+  try
+    let res = fn arg1 arg2 arg3 arg4 in
+    add_to_timer name (Unix.gettimeofday() -. start);
+    res
+  with x ->
+    add_to_timer name (Unix.gettimeofday() -. start);
+    raise x
+
 let print_timers () =
   Hashtbl.iter
     (fun name time -> Printf.printf "%-20s %.3f\n" name time)
diff --git a/lib/Integers.v b/lib/Integers.v
index cbbf28c..d85007b 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -2454,6 +2454,19 @@ Proof.
   generalize wordsize_pos; generalize wordsize_max_unsigned; omega. 
 Qed.
 
+Theorem ror_rol_neg:
+  forall x y, (zwordsize | modulus) -> ror x y = rol x (neg y).
+Proof.
+  intros. apply same_bits_eq; intros.
+  rewrite bits_ror by auto. rewrite bits_rol by auto. 
+  f_equal. apply eqmod_mod_eq. omega. 
+  apply eqmod_trans with (i - (- unsigned y)). 
+  apply eqmod_refl2; omega. 
+  apply eqmod_sub. apply eqmod_refl.
+  apply eqmod_divides with modulus. 
+  apply eqm_unsigned_repr. auto.
+Qed.
+
 Theorem or_ror:
   forall x y z,
   ltu y iwordsize = true ->
diff --git a/lib/IntvSets.v b/lib/IntvSets.v
new file mode 100644
index 0000000..9f1a895
--- /dev/null
+++ b/lib/IntvSets.v
@@ -0,0 +1,410 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Finite sets of integer intervals *)
+
+Require Import Coqlib.
+
+Module ISet.
+
+(** "Raw", non-dependent implementation.  A set of intervals is a
+  list of nonempty semi-open intervals [(lo, hi)],
+  sorted in increasing order of the low bound,
+  and with no overlap nor adjacency between elements.
+  In particular, if the list contains [(lo1, hi1)] followed by [(lo2, hi2)],
+  we have [lo1 < hi1 < lo2 < hi2]. *)
+
+Module R.
+
+Inductive t : Type := Nil | Cons (lo hi: Z) (tl: t).
+
+Fixpoint In (x: Z) (s: t) :=
+  match s with
+  | Nil => False
+  | Cons l h s' => l <= x < h \/ In x s'
+  end.
+
+Inductive ok: t -> Prop :=
+  | ok_nil: ok Nil
+  | ok_cons: forall l h s
+      (BOUNDS: l < h)
+      (BELOW: forall x, In x s -> h < x)
+      (OK: ok s),
+      ok (Cons l h s).
+
+Fixpoint mem (x: Z) (s: t) : bool :=
+  match s with
+  | Nil => false
+  | Cons l h s' => if zlt x h then zle l x else mem x s'
+  end.
+
+Lemma mem_In:
+  forall x s, ok s -> (mem x s = true <-> In x s).
+Proof.
+  induction 1; simpl.
+- intuition congruence.
+- destruct (zlt x h). 
++ destruct (zle l x); simpl.
+  * tauto.
+  * split; intros. congruence.
+    exfalso. destruct H0. omega. exploit BELOW; eauto. omega. 
++ rewrite IHok. intuition. 
+Qed.
+
+Fixpoint contains (L H: Z) (s: t) : bool :=
+  match s with
+  | Nil => false
+  | Cons l h s' => (zle H h && zle l L) || contains L H s'
+  end.
+
+Lemma contains_In:
+  forall l0 h0, l0 < h0 -> forall s, ok s ->
+  (contains l0 h0 s = true <-> (forall x, l0 <= x < h0 -> In x s)).
+Proof.
+  induction 2; simpl.
+- intuition. elim (H0 l0); omega.
+- destruct (zle h0 h); simpl.
+  destruct (zle l l0); simpl.
+  intuition.
+  rewrite IHok. intuition. destruct (H3 x); auto. exfalso. 
+  destruct (H3 l0). omega. omega. exploit BELOW; eauto. omega.
+  rewrite IHok. intuition. destruct (H3 x); auto. exfalso. 
+  destruct (H3 h). omega. omega. exploit BELOW; eauto. omega.
+Qed.
+
+Fixpoint add (L H: Z) (s: t) {struct s} : t :=
+  match s with
+  | Nil => Cons L H Nil
+  | Cons l h s' =>
+      if zlt h L then Cons l h (add L H s')
+      else if zlt H l then Cons L H s
+      else add (Z.min l L) (Z.max h H) s'
+  end.
+
+Lemma In_add:
+  forall x s, ok s -> forall l0 h0, (In x (add l0 h0 s) <-> l0 <= x < h0 \/ In x s).
+Proof.
+  induction 1; simpl; intros.
+  tauto.
+  destruct (zlt h l0).
+  simpl. rewrite IHok. tauto.
+  destruct (zlt h0 l).
+  simpl. tauto.
+  rewrite IHok. intuition. 
+  assert (l0 <= x < h0 \/ l <= x < h) by xomega. tauto.
+  left; xomega.
+  left; xomega.
+Qed.
+
+Lemma add_ok:
+  forall s, ok s -> forall l0 h0, l0 < h0 -> ok (add l0 h0 s).
+Proof.
+  induction 1; simpl; intros.
+  constructor. auto. intros. inv H0. constructor.
+  destruct (zlt h l0).
+  constructor; auto. intros. rewrite In_add in H1; auto.
+  destruct H1. omega. auto. 
+  destruct (zlt h0 l).
+  constructor. auto. simpl; intros. destruct H1. omega. exploit BELOW; eauto. omega. 
+  constructor. omega. auto. auto. 
+  apply IHok. xomega.
+Qed.
+
+Fixpoint remove (L H: Z) (s: t) {struct s} : t :=
+  match s with
+  | Nil => Nil
+  | Cons l h s' =>
+      if zlt h L then Cons l h (remove L H s')
+      else if zlt H l then s
+      else if zlt l L then
+        if zlt H h then Cons l L (Cons H h s') else Cons l L (remove L H s')
+      else 
+        if zlt H h then Cons H h s' else remove L H s'
+  end.
+
+Lemma In_remove:
+  forall x l0 h0 s, ok s ->
+  (In x (remove l0 h0 s) <-> ~(l0 <= x < h0) /\ In x s).
+Proof.
+  induction 1; simpl.
+  tauto.
+  destruct (zlt h l0).
+  simpl. rewrite IHok. intuition omega. 
+  destruct (zlt h0 l).
+  simpl. intuition. exploit BELOW; eauto. omega. 
+  destruct (zlt l l0).
+  destruct (zlt h0 h); simpl. clear IHok. split.
+  intros [A | [A | A]]. 
+  split. omega. left; omega. 
+  split. omega. left; omega. 
+  split. exploit BELOW; eauto. omega. auto.
+  intros [A [B | B]].
+  destruct (zlt x l0). left; omega. right; left; omega. 
+  auto.
+  intuition omega. 
+  destruct (zlt h0 h); simpl.
+  intuition. exploit BELOW; eauto. omega.
+  rewrite IHok. intuition. omegaContradiction. 
+Qed.
+
+Lemma remove_ok:
+  forall l0 h0, l0 < h0 -> forall s, ok s -> ok (remove l0 h0 s).
+Proof.
+  induction 2; simpl.
+  constructor.
+  destruct (zlt h l0).
+  constructor; auto. intros; apply BELOW. rewrite In_remove in H1; tauto. 
+  destruct (zlt h0 l).
+  constructor; auto. 
+  destruct (zlt l l0).
+  destruct (zlt h0 h).
+  constructor. omega. intros. inv H1. omega. exploit BELOW; eauto. omega. 
+  constructor. omega. auto. auto.
+  constructor; auto. intros. rewrite In_remove in H1 by auto. destruct H1. exploit BELOW; eauto. omega. 
+  destruct (zlt h0 h).
+  constructor; auto.
+  auto.
+Qed.
+
+Fixpoint inter (s1 s2: t) {struct s1} : t :=
+  let fix intr (s2: t) : t :=
+    match s1, s2 with
+    | Nil, _ => Nil
+    | _, Nil => Nil
+    | Cons l1 h1 s1', Cons l2 h2 s2' =>
+        if zle h1 l2 then inter s1' s2
+        else if zle h2 l1 then intr s2'
+        else if zle l1 l2 then
+          if zle h2 h1 then Cons l2 h2 (intr s2') else Cons l2 h1 (inter s1' s2)
+        else
+          if zle h1 h2 then Cons l1 h1 (inter s1' s2) else Cons l1 h2 (intr s2')
+    end
+  in intr s2.
+
+Lemma In_inter:
+  forall x s1, ok s1 -> forall s2, ok s2 ->
+  (In x (inter s1 s2) <-> In x s1 /\ In x s2).
+Proof.
+  induction 1.
+  simpl. induction 1; simpl. tauto. tauto.
+  assert (ok (Cons l h s)) by (constructor; auto).
+  induction 1; simpl.
+  tauto.
+  assert (ok (Cons l0 h0 s0)) by (constructor; auto).
+  destruct (zle h l0).
+  rewrite IHok; auto. simpl. intuition. omegaContradiction. 
+  exploit BELOW0; eauto. intros. omegaContradiction.
+  destruct (zle h0 l).
+  simpl in IHok0; rewrite IHok0. intuition. omegaContradiction.
+  exploit BELOW; eauto. intros; omegaContradiction.
+  destruct (zle l l0).
+  destruct (zle h0 h).
+  simpl. simpl in IHok0; rewrite IHok0. intuition.
+  simpl. rewrite IHok; auto. simpl. intuition.  exploit BELOW0; eauto. intros; omegaContradiction. 
+  destruct (zle h h0).
+  simpl. rewrite IHok; auto. simpl. intuition.
+  simpl. simpl in IHok0; rewrite IHok0. intuition. 
+  exploit BELOW; eauto. intros; omegaContradiction.
+Qed.
+
+Lemma inter_ok:
+  forall s1, ok s1 -> forall s2, ok s2 -> ok (inter s1 s2).
+Proof.
+  induction 1.
+  intros; simpl. destruct s2; constructor.
+  assert (ok (Cons l h s)). constructor; auto.
+  induction 1; simpl.
+  constructor.
+  assert (ok (Cons l0 h0 s0)). constructor; auto.
+  destruct (zle h l0).
+  auto.
+  destruct (zle h0 l).
+  auto.
+  destruct (zle l l0).
+  destruct (zle h0 h).
+  constructor; auto. intros.
+  assert (In x (inter (Cons l h s) s0)) by exact H3.
+  rewrite In_inter in H4; auto. apply BELOW0. tauto.
+  constructor. omega. intros. rewrite In_inter in H3; auto. apply BELOW. tauto. 
+  auto. 
+  destruct (zle h h0).
+  constructor. omega. intros. rewrite In_inter in H3; auto. apply BELOW. tauto.
+  auto.
+  constructor. omega. intros.
+  assert (In x (inter (Cons l h s) s0)) by exact H3.
+  rewrite In_inter in H4; auto. apply BELOW0. tauto.
+  auto.
+Qed.
+
+Fixpoint union (s1 s2: t) : t :=
+  match s1, s2 with
+  | Nil, _ => s2
+  | _, Nil => s1
+  | Cons l1 h1 s1', Cons l2 h2 s2' => add l1 h1 (add l2 h2 (union s1' s2'))
+  end.
+
+Lemma In_ok_union:
+  forall s1, ok s1 -> forall s2, ok s2 ->
+  ok (union s1 s2) /\ (forall x, In x s1 \/ In x s2 <-> In x (union s1 s2)).
+Proof.
+  induction 1; destruct 1; simpl.
+  split. constructor. tauto.
+  split. constructor; auto. tauto.
+  split. constructor; auto. tauto.
+  destruct (IHok s0) as [A B]; auto.
+  split. apply add_ok; auto. apply add_ok; auto.
+  intros. rewrite In_add. rewrite In_add. rewrite <- B. tauto. auto. apply add_ok; auto. 
+Qed.
+
+Fixpoint beq (s1 s2: t) : bool :=
+  match s1, s2 with
+  | Nil, Nil => true
+  | Cons l1 h1 t1, Cons l2 h2 t2 => zeq l1 l2 && zeq h1 h2 && beq t1 t2
+  | _, _ => false
+  end.
+
+Lemma beq_spec:
+  forall s1, ok s1 -> forall s2, ok s2 ->
+  (beq s1 s2 = true <-> (forall x, In x s1 <-> In x s2)).
+Proof.
+  induction 1; destruct 1; simpl.
+- tauto.
+- split; intros. discriminate. exfalso. apply (H0 l). left; omega. 
+- split; intros. discriminate. exfalso. apply (H0 l). left; omega.
+- split; intros. 
++ InvBooleans. subst. rewrite IHok in H3 by auto. rewrite H3. tauto. 
++ destruct (zeq l l0). destruct (zeq h h0). simpl. subst. 
+  apply IHok. auto. intros; split; intros.
+  destruct (proj1 (H1 x)); auto. exfalso. exploit BELOW; eauto. omega. 
+  destruct (proj2 (H1 x)); auto. exfalso. exploit BELOW0; eauto. omega.
+  exfalso. subst l0. destruct (zlt h h0).
+  destruct (proj2 (H1 h)). left; omega. omega. exploit BELOW; eauto. omega.
+  destruct (proj1 (H1 h0)). left; omega. omega. exploit BELOW0; eauto. omega.
+  exfalso. destruct (zlt l l0).
+  destruct (proj1 (H1 l)). left; omega. omega. exploit BELOW0; eauto. omega.
+  destruct (proj2 (H1 l0)). left; omega. omega. exploit BELOW; eauto. omega.
+Qed.
+
+End R.
+
+(** Exported interface, wrapping the [ok] invariant in a dependent type. *)
+
+Definition t := { r: R.t | R.ok r }.
+
+Program Definition In (x: Z) (s: t) := R.In x s.
+
+Program Definition empty : t := R.Nil.
+Next Obligation. constructor. Qed.
+
+Theorem In_empty: forall x, ~(In x empty).
+Proof.
+  unfold In; intros; simpl. tauto. 
+Qed.
+
+Program Definition interval (l h: Z) : t :=
+  if zlt l h then R.Cons l h R.Nil else R.Nil.
+Next Obligation.
+  constructor; auto. simpl; tauto. constructor.
+Qed.
+Next Obligation.
+  constructor.
+Qed.
+
+Theorem In_interval: forall x l h, In x (interval l h) <-> l <= x < h.
+Proof.
+  intros. unfold In, interval; destruct (zlt l h); simpl.
+  intuition.
+  intuition.
+Qed.
+
+Program Definition add (l h: Z) (s: t) : t :=
+  if zlt l h then R.add l h s else s.
+Next Obligation.
+  apply R.add_ok. apply proj2_sig. auto.
+Qed.
+
+Theorem In_add: forall x l h s, In x (add l h s) <-> l <= x < h \/ In x s.
+Proof.
+  unfold add, In; intros. 
+  destruct (zlt l h).
+  simpl. apply R.In_add. apply proj2_sig.
+  intuition. omegaContradiction. 
+Qed.
+
+Program Definition remove (l h: Z) (s: t) : t :=
+  if zlt l h then R.remove l h s else s.
+Next Obligation.
+  apply R.remove_ok. auto. apply proj2_sig. 
+Qed.
+
+Theorem In_remove: forall x l h s, In x (remove l h s) <-> ~(l <= x < h) /\ In x s.
+Proof.
+  unfold remove, In; intros.
+  destruct (zlt l h).
+  simpl. apply R.In_remove. apply proj2_sig.
+  intuition.
+Qed.
+
+Program Definition inter (s1 s2: t) : t := R.inter s1 s2.
+Next Obligation. apply R.inter_ok; apply proj2_sig. Qed.
+
+Theorem In_inter: forall x s1 s2, In x (inter s1 s2) <-> In x s1 /\ In x s2.
+Proof.
+  unfold inter, In; intros; simpl. apply R.In_inter; apply proj2_sig. 
+Qed.
+
+Program Definition union (s1 s2: t) : t := R.union s1 s2.
+Next Obligation. 
+  destruct (R.In_ok_union _ (proj2_sig s1) _ (proj2_sig s2)). auto.
+Qed.
+
+Theorem In_union: forall x s1 s2, In x (union s1 s2) <-> In x s1 \/ In x s2.
+Proof.
+  unfold union, In; intros; simpl.
+  destruct (R.In_ok_union _ (proj2_sig s1) _ (proj2_sig s2)).
+  generalize (H0 x); tauto.
+Qed.
+
+Program Definition mem (x: Z) (s: t) := R.mem x s.
+
+Theorem mem_spec: forall x s, mem x s = true <-> In x s.
+Proof.
+  unfold mem, In; intros. apply R.mem_In. apply proj2_sig. 
+Qed.
+
+Program Definition contains (l h: Z) (s: t) :=
+  if zlt l h then R.contains l h s else true.
+
+Theorem contains_spec:
+  forall l h s, contains l h s = true <-> (forall x, l <= x < h -> In x s).
+Proof.
+  unfold contains, In; intros. destruct (zlt l h).
+  apply R.contains_In. auto. apply proj2_sig.
+  split; intros. omegaContradiction. auto. 
+Qed.
+
+Program Definition beq (s1 s2: t) : bool := R.beq s1 s2.
+
+Theorem beq_spec:
+  forall s1 s2, beq s1 s2 = true <-> (forall x, In x s1 <-> In x s2).
+Proof.
+  unfold mem, In; intros. apply R.beq_spec; apply proj2_sig.
+Qed.
+
+End ISet.
+
+
+
+
diff --git a/lib/Lattice.v b/lib/Lattice.v
index cb28b5b..5a941a1 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -66,42 +66,28 @@ End SEMILATTICE_WITH_TOP.
 
 Set Implicit Arguments.
 
-(** Given a semi-lattice with top [L], the following functor implements
+(** Given a semi-lattice (without top) [L], the following functor implements
   a semi-lattice structure over finite maps from positive numbers to [L.t].
-  The default value for these maps is either [L.top] or [L.bot]. *)
-
-Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP.
+  The default value for these maps is [L.bot].  Bottom elements are not smashed. *)
 
-Inductive t' : Type :=
-  | Bot: t'
-  | Top_except: PTree.t L.t -> t'.
+Module LPMap1(L: SEMILATTICE) <: SEMILATTICE.
 
-Definition t: Type := t'.
+Definition t := PTree.t L.t.
 
 Definition get (p: positive) (x: t) : L.t :=
-  match x with
-  | Bot => L.bot
-  | Top_except m => match m!p with None => L.top | Some x => x end
-  end.
+  match x!p with None => L.bot | Some x => x end.
 
 Definition set (p: positive) (v: L.t) (x: t) : t :=
-  match x with
-  | Bot => Bot
-  | Top_except m =>
-      if L.beq v L.bot
-      then Bot
-      else Top_except (if L.beq v L.top then PTree.remove p m else PTree.set p v m)
-  end.
+  if L.beq v L.bot
+  then PTree.remove p x
+  else PTree.set p v x.
 
 Lemma gsspec:
   forall p v x q,
-  x <> Bot -> ~L.eq v L.bot ->
   L.eq (get q (set p v x)) (if peq q p then v else get q x).
 Proof.
-  intros. unfold set. destruct x. congruence. 
-  destruct (L.beq v L.bot) eqn:EBOT. 
-  elim H0. apply L.beq_correct; auto.
-  destruct (L.beq v L.top) eqn:ETOP; simpl.
+  intros. unfold set, get. 
+  destruct (L.beq v L.bot) eqn:EBOT.
   rewrite PTree.grspec. unfold PTree.elt_eq. destruct (peq q p). 
   apply L.eq_sym. apply L.beq_correct; auto.
   apply L.eq_refl.
@@ -126,20 +112,13 @@ Proof.
   unfold eq; intros. eapply L.eq_trans; eauto.
 Qed.
 
-Definition beq (x y: t) : bool :=
-  match x, y with
-  | Bot, Bot => true
-  | Top_except m, Top_except n => PTree.beq L.beq m n
-  | _, _ => false
-  end.
+Definition beq (x y: t) : bool := PTree.beq L.beq x y.
 
 Lemma beq_correct: forall x y, beq x y = true -> eq x y.
 Proof.
-  destruct x; destruct y; simpl; intro; try congruence.
-  apply eq_refl.
-  red; intro; simpl.
-  rewrite PTree.beq_correct in H. generalize (H p).
-  destruct (t0!p); destruct (t1!p); intuition.
+  unfold beq; intros; red; intros. unfold get.
+  rewrite PTree.beq_correct in H. specialize (H p). 
+  destruct (x!p); destruct (y!p); intuition.
   apply L.beq_correct; auto.
   apply L.eq_refl.
 Qed.
@@ -157,11 +136,11 @@ Proof.
   unfold ge; intros. apply L.ge_trans with (get p y); auto.
 Qed.
 
-Definition bot := Bot.
+Definition bot : t := PTree.empty _.
 
 Lemma get_bot: forall p, get p bot = L.bot.
 Proof.
-  unfold bot; intros; simpl. auto.
+  unfold bot, get; intros; simpl. rewrite PTree.gempty. auto.
 Qed.
 
 Lemma ge_bot: forall x, ge x bot.
@@ -169,18 +148,6 @@ Proof.
   unfold ge; intros. rewrite get_bot. apply L.ge_bot.
 Qed.
 
-Definition top := Top_except (PTree.empty L.t).
-
-Lemma get_top: forall p, get p top = L.top.
-Proof.
-  unfold top; intros; simpl. rewrite PTree.gempty. auto.
-Qed.
-
-Lemma ge_top: forall x, ge top x.
-Proof.
-  unfold ge; intros. rewrite get_top. apply L.ge_top.
-Qed.
-
 (** A [combine] operation over the type [PTree.t L.t] that attempts
   to share its result with its arguments. *)
 
@@ -407,6 +374,168 @@ Qed.
 
 End COMBINE.
 
+Definition lub (x y: t) : t :=
+  combine
+    (fun a b =>
+       match a, b with
+       | Some u, Some v => Some (L.lub u v)
+       | None, _ => b
+       | _, None => a
+       end)
+    x y.
+
+Lemma gcombine_bot:
+  forall f t1 t2 p,
+  f None None = None ->
+  L.eq (get p (combine f t1 t2))
+       (match f t1!p t2!p with Some x => x | None => L.bot end).
+Proof.
+  intros. unfold get. generalize (gcombine f H t1 t2 p). unfold opt_eq. 
+  destruct ((combine f t1 t2)!p); destruct (f t1!p t2!p).
+  auto. contradiction. contradiction. intros; apply L.eq_refl.
+Qed.
+
+Lemma ge_lub_left:
+  forall x y, ge (lub x y) x.
+Proof.
+  unfold ge, lub; intros. 
+  eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot; auto.
+  unfold get. destruct x!p. destruct y!p. 
+  apply L.ge_lub_left.
+  apply L.ge_refl. apply L.eq_refl.
+  apply L.ge_bot.
+Qed.
+
+Lemma ge_lub_right:
+  forall x y, ge (lub x y) y.
+Proof.
+  unfold ge, lub; intros. 
+  eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot; auto.
+  unfold get. destruct y!p. destruct x!p. 
+  apply L.ge_lub_right.
+  apply L.ge_refl. apply L.eq_refl.
+  apply L.ge_bot.
+Qed.
+
+End LPMap1.
+
+(** Given a semi-lattice with top [L], the following functor implements
+  a semi-lattice-with-top structure over finite maps from positive numbers to [L.t].
+  The default value for these maps is [L.top].  Bottom elements are smashed. *)
+
+Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP.
+
+Inductive t' : Type :=
+  | Bot: t'
+  | Top_except: PTree.t L.t -> t'.
+
+Definition t: Type := t'.
+
+Definition get (p: positive) (x: t) : L.t :=
+  match x with
+  | Bot => L.bot
+  | Top_except m => match m!p with None => L.top | Some x => x end
+  end.
+
+Definition set (p: positive) (v: L.t) (x: t) : t :=
+  match x with
+  | Bot => Bot
+  | Top_except m =>
+      if L.beq v L.bot
+      then Bot
+      else Top_except (if L.beq v L.top then PTree.remove p m else PTree.set p v m)
+  end.
+
+Lemma gsspec:
+  forall p v x q,
+  x <> Bot -> ~L.eq v L.bot ->
+  L.eq (get q (set p v x)) (if peq q p then v else get q x).
+Proof.
+  intros. unfold set. destruct x. congruence. 
+  destruct (L.beq v L.bot) eqn:EBOT. 
+  elim H0. apply L.beq_correct; auto.
+  destruct (L.beq v L.top) eqn:ETOP; simpl.
+  rewrite PTree.grspec. unfold PTree.elt_eq. destruct (peq q p). 
+  apply L.eq_sym. apply L.beq_correct; auto.
+  apply L.eq_refl.
+  rewrite PTree.gsspec. destruct (peq q p); apply L.eq_refl.
+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, Bot => true
+  | 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.
+  apply eq_refl.
+  red; intro; simpl.
+  rewrite PTree.beq_correct in H. generalize (H p).
+  destruct (t0!p); destruct (t1!p); intuition.
+  apply L.beq_correct; auto.
+  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 y, eq x y -> ge x y.
+Proof.
+  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.
+Proof.
+  unfold ge; intros. apply L.ge_trans with (get p y); auto.
+Qed.
+
+Definition bot := Bot.
+
+Lemma get_bot: forall p, get p bot = L.bot.
+Proof.
+  unfold bot; intros; simpl. auto.
+Qed.
+
+Lemma ge_bot: forall x, ge x bot.
+Proof.
+  unfold ge; intros. rewrite get_bot. apply L.ge_bot.
+Qed.
+
+Definition top := Top_except (PTree.empty L.t).
+
+Lemma get_top: forall p, get p top = L.top.
+Proof.
+  unfold top; intros; simpl. rewrite PTree.gempty. auto.
+Qed.
+
+Lemma ge_top: forall x, ge top x.
+Proof.
+  unfold ge; intros. rewrite get_top. apply L.ge_top.
+Qed.
+
+Module LM := LPMap1(L).
+
 Definition opt_lub (x y: L.t) : option L.t :=
   let z := L.lub x y in
   if L.beq z L.top then None else Some z.
@@ -417,7 +546,7 @@ Definition lub (x y: t) : t :=
   | _, Bot => x
   | Top_except m, Top_except n =>
       Top_except
-        (combine
+        (LM.combine
            (fun a b =>
               match a, b with
               | Some u, Some v => opt_lub u v
@@ -429,11 +558,11 @@ Definition lub (x y: t) : t :=
 Lemma gcombine_top:
   forall f t1 t2 p,
   f None None = None ->
-  L.eq (get p (Top_except (combine f t1 t2)))
+  L.eq (get p (Top_except (LM.combine f t1 t2)))
        (match f t1!p t2!p with Some x => x | None => L.top end).
 Proof.
-  intros. simpl. generalize (gcombine f H t1 t2 p). unfold opt_eq. 
-  destruct ((combine f t1 t2)!p); destruct (f t1!p t2!p).
+  intros. simpl. generalize (LM.gcombine f H t1 t2 p). unfold LM.opt_eq. 
+  destruct ((LM.combine f t1 t2)!p); destruct (f t1!p t2!p).
   auto. contradiction. contradiction. intros; apply L.eq_refl.
 Qed.