stuff information into a record

2 files changed, 63 insertions, 46 deletions

diff --git a/backend/CSE2.v b/backend/CSE2.v
index b7665097..0479dad9 100644
--- a/backend/CSE2.v
+++ b/backend/CSE2.v
@@ -29,13 +29,18 @@ Proof.
   decide equality.
 Defined.
 
+Record relmap := mkrel {
+              var_to_sym : (PTree.t sym_val)
+                   }.
+
 Module RELATION.
-  
-Definition t := (PTree.t sym_val).
+
+Definition t := relmap.
+
 Definition eq (r1 r2 : t) :=
-  forall x, (PTree.get x r1) = (PTree.get x r2).
+  forall x, (PTree.get x (var_to_sym r1)) = (PTree.get x (var_to_sym r2)).
 
-Definition top : t := PTree.empty sym_val.
+Definition top : t := mkrel (PTree.empty sym_val).
 
 Lemma eq_refl: forall x, eq x x.
 Proof.
@@ -58,27 +63,27 @@ Qed.
 Definition sym_val_beq (x y : sym_val) :=
   if eq_sym_val x y then true else false.
 
-Definition beq (r1 r2 : t) := PTree.beq sym_val_beq r1 r2.
+Definition beq (r1 r2 : t) := PTree.beq sym_val_beq (var_to_sym r1) (var_to_sym r2).
 
 Lemma beq_correct: forall r1 r2, beq r1 r2 = true -> eq r1 r2.
 Proof.
   unfold beq, eq. intros r1 r2 EQ x.
-  pose proof (PTree.beq_correct sym_val_beq r1 r2) as CORRECT.
+  pose proof (PTree.beq_correct sym_val_beq (var_to_sym r1) (var_to_sym r2)) as CORRECT.
   destruct CORRECT as [CORRECTF CORRECTB].
   pose proof (CORRECTF EQ x) as EQx.
   clear CORRECTF CORRECTB EQ.
   unfold sym_val_beq in *.
-  destruct (r1 ! x) as [R1x | ] in *;
-    destruct (r2 ! x) as [R2x | ] in *;
+  destruct ((var_to_sym r1) ! x) as [R1x | ] in *;
+    destruct ((var_to_sym r2) ! x) as [R2x | ] in *;
     trivial; try contradiction.
   destruct (eq_sym_val R1x R2x) in *; congruence.
 Qed.
 
 Definition ge (r1 r2 : t) :=
   forall x,
-    match PTree.get x r1 with
+    match PTree.get x (var_to_sym r1) with
     | None => True
-    | Some v => (PTree.get x r2) = Some v
+    | Some v => (PTree.get x (var_to_sym r2)) = Some v
     end.
 
 Lemma ge_refl: forall r1 r2, eq r1 r2 -> ge r1 r2.
@@ -87,7 +92,7 @@ Proof.
   intros r1 r2 EQ x.
   pose proof (EQ x) as EQx.
   clear EQ.
-  destruct (r1 ! x).
+  destruct ((var_to_sym r1) ! x).
   - congruence.
   - trivial.
 Qed.
@@ -98,12 +103,13 @@ Proof.
   intros r1 r2 r3 GE12 GE23 x.
   pose proof (GE12 x) as GE12x; clear GE12.
   pose proof (GE23 x) as GE23x; clear GE23.
-  destruct (r1 ! x); trivial.
-  destruct (r2 ! x); congruence.
+  destruct ((var_to_sym r1) ! x); trivial.
+  destruct ((var_to_sym r2) ! x); congruence.
 Qed.
 
 Definition lub (r1 r2 : t) :=
-  PTree.combine
+  mkrel
+  (PTree.combine
     (fun ov1 ov2 =>
        match ov1, ov2 with
        | (Some v1), (Some v2) =>
@@ -113,12 +119,12 @@ Definition lub (r1 r2 : t) :=
        | None, _
        | _, None => None
        end)
-    r1 r2.
+    (var_to_sym r1) (var_to_sym r2)).
 
 Lemma ge_lub_left: forall x y, ge (lub x y) x.
 Proof.
   unfold ge, lub.
-  intros r1 r2 x.
+  intros r1 r2 x. simpl.
   rewrite PTree.gcombine by reflexivity.
   destruct (_ ! _); trivial.
   destruct (_ ! _); trivial.
@@ -128,7 +134,7 @@ Qed.
 Lemma ge_lub_right: forall x y, ge (lub x y) y.
 Proof.
   unfold ge, lub.
-  intros r1 r2 x.
+  intros r1 r2 x. simpl.
   rewrite PTree.gcombine by reflexivity.
   destruct (_ ! _); trivial.
   destruct (_ ! _); trivial.
@@ -263,8 +269,8 @@ Definition kill_sym_val (dst : reg) (sv : sym_val) :=
   end.
                                                  
 Definition kill_reg (dst : reg) (rel : RELATION.t) :=
-  PTree.filter1 (fun x => negb (kill_sym_val dst x))
-                (PTree.remove dst rel).
+  mkrel (PTree.filter1 (fun x => negb (kill_sym_val dst x))
+                       (PTree.remove dst (var_to_sym rel))).
 
 Definition kill_sym_val_mem (sv: sym_val) :=
   match sv with
@@ -274,17 +280,18 @@ Definition kill_sym_val_mem (sv: sym_val) :=
   end.
 
 Definition kill_mem (rel : RELATION.t) :=
-  PTree.filter1 (fun x => negb (kill_sym_val_mem x)) rel.
+  mkrel
+    (PTree.filter1 (fun x => negb (kill_sym_val_mem x)) (var_to_sym rel)).
 
 
 Definition forward_move (rel : RELATION.t) (x : reg) : reg :=
-  match rel ! x with
+  match (var_to_sym rel) ! x with
   | Some (SMove org) => org
   | _ => x
   end.
 
 Definition move (src dst : reg) (rel : RELATION.t) :=
-  PTree.set dst (SMove (forward_move rel src)) (kill_reg dst rel).
+  mkrel (PTree.set dst (SMove (forward_move rel src)) (var_to_sym (kill_reg dst rel))).
 
 Definition find_op_fold op args (already : option reg) x sv :=
                 match already with
@@ -300,7 +307,7 @@ Definition find_op_fold op args (already : option reg) x sv :=
                 end.
 
 Definition find_op (rel : RELATION.t) (op : operation) (args : list reg) :=
-  PTree.fold (find_op_fold op args) rel None.
+  PTree.fold (find_op_fold op args) (var_to_sym rel) None.
 
 Definition find_load_fold chunk addr args (already : option reg) x sv :=
                 match already with
@@ -318,12 +325,12 @@ Definition find_load_fold chunk addr args (already : option reg) x sv :=
                 end.
 
 Definition find_load (rel : RELATION.t) (chunk : memory_chunk) (addr : addressing) (args : list reg) :=
-  PTree.fold (find_load_fold chunk addr args) rel None.
+  PTree.fold (find_load_fold chunk addr args) (var_to_sym rel) None.
 
 Definition oper2 (op: operation) (dst : reg) (args : list reg)
            (rel : RELATION.t) :=
   let rel' := kill_reg dst rel in
-  PTree.set dst (SOp op (List.map (forward_move rel') args)) rel'.
+  mkrel (PTree.set dst (SOp op (List.map (forward_move rel') args)) (var_to_sym rel')).
 
 Definition oper1 (op: operation) (dst : reg) (args : list reg)
            (rel : RELATION.t) :=
@@ -348,7 +355,7 @@ Definition gen_oper (op: operation) (dst : reg) (args : list reg)
 Definition load2 (chunk: memory_chunk) (addr : addressing)
            (dst : reg) (args : list reg) (rel : RELATION.t) :=
   let rel' := kill_reg dst rel in
-  PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) rel'.
+  mkrel (PTree.set dst (SLoad chunk addr (List.map (forward_move rel') args)) (var_to_sym rel')).
 
 Definition load1 (chunk: memory_chunk) (addr : addressing)
            (dst : reg) (args : list reg) (rel : RELATION.t) :=
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 82fa8a28..a29bf202 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -58,7 +58,7 @@ Definition sem_sym_val sym rs (v : option val) : Prop :=
   end.
     
 Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) (v : val) : Prop :=
-  match rel ! x with
+  match (var_to_sym rel) ! x with
   | None => True
   | Some sym => sem_sym_val sym rs (Some (rs # x)) 
   end.
@@ -98,7 +98,7 @@ Proof.
   pose proof (SEM arg) as SEMarg.
   simpl. unfold forward_move.
   unfold sem_sym_val in *.
-  destruct (t ! arg); trivial.
+  destruct (_ ! arg); trivial.
   destruct s; congruence.
 Qed.
 
@@ -127,7 +127,7 @@ Lemma kill_reg_sound :
 Proof.
   unfold sem_rel, kill_reg, sem_reg, sem_sym_val.
   intros until v.
-  intros REL x.
+  intros REL x. simpl.
   rewrite PTree.gfilter1.
   destruct (Pos.eq_dec dst x).
   {
@@ -137,7 +137,7 @@ Proof.
   }
   rewrite PTree.gro by congruence.
   rewrite Regmap.gso by congruence.
-  destruct (rel ! x) as [relx | ] eqn:RELx; trivial.
+  destruct (_ ! x) as [relx | ] eqn:RELx; trivial.
   unfold kill_sym_val.
   pose proof (REL x) as RELinstx.
   rewrite RELx in RELinstx.
@@ -190,12 +190,13 @@ Proof.
   {
     subst x.
     unfold sem_reg.
+    simpl.
     rewrite PTree.gss.
     rewrite Regmap.gss.
     unfold sem_reg in *.
     simpl.
     unfold forward_move.
-    destruct (rel ! src) as [ sv |]; simpl.
+    destruct (_ ! src) as [ sv |]; simpl.
     destruct sv eqn:SV; simpl in *.
     {
       destruct (peq dst src0).
@@ -211,6 +212,7 @@ Proof.
   }
   rewrite Regmap.gso by congruence.
   unfold sem_reg.
+  simpl.
   rewrite PTree.gso by congruence.
   rewrite Regmap.gso in KILL by congruence.
   exact KILL.
@@ -223,9 +225,10 @@ Lemma move_cases_neq:
 Proof.
   intros until a. intro NEQ.
   unfold kill_reg, forward_move.
+  simpl.
   rewrite PTree.gfilter1.
   rewrite PTree.gro by congruence.
-  destruct (rel ! a); simpl.
+  destruct (_ ! a); simpl.
   2: congruence.
   destruct s.
   {
@@ -259,9 +262,10 @@ Proof.
   unfold kill_reg.
   unfold sem_reg in RELa.
   unfold forward_move.
+  simpl.
   rewrite PTree.gfilter1.
   rewrite PTree.gro by auto.
-  destruct (rel ! a); simpl; trivial.
+  destruct (_ ! a); simpl; trivial.
   destruct s; simpl in *; destruct negb; simpl; congruence.
 Qed.
 
@@ -285,6 +289,7 @@ Proof.
   {
     subst x.
     unfold sem_reg.
+    simpl.
     rewrite PTree.gss.
     rewrite Regmap.gss.
     simpl.
@@ -294,6 +299,7 @@ Proof.
   }
   rewrite Regmap.gso by congruence.
   unfold sem_reg.
+  simpl.
   rewrite PTree.gso by congruence.
   rewrite Regmap.gso in KILL by congruence.
   exact KILL.
@@ -341,13 +347,13 @@ Proof.
              | Some src => eval_operation genv sp op rs ## args m = Some rs # src
              end -> fold_left
     (fun (a : option reg) (p : positive * sym_val) =>
-     find_op_fold op args a (fst p) (snd p)) (PTree.elements rel) start =
+     find_op_fold op args a (fst p) (snd p)) (PTree.elements (var_to_sym rel)) start =
                     Some src ->
              eval_operation genv sp op rs ## args m = Some rs # src) as REC.
   {
     unfold sem_rel, sem_reg in REL.
-    generalize (PTree.elements_complete rel).
-    generalize (PTree.elements rel).
+    generalize (PTree.elements_complete (var_to_sym rel)).
+    generalize (PTree.elements (var_to_sym rel)).
     induction l; simpl.
     {
       intros.
@@ -372,7 +378,7 @@ Proof.
     destruct eq_args; trivial.
     subst args0.
     simpl.
-    assert ((rel ! r) = Some (SOp op args)) as RELatr.
+    assert (((var_to_sym rel) ! r) = Some (SOp op args)) as RELatr.
     {
       apply COMPLETE.
       left.
@@ -417,7 +423,7 @@ Proof.
              end ->
     fold_left
     (fun (a : option reg) (p : positive * sym_val) =>
-     find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements rel) start =
+     find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements (var_to_sym rel)) start =
     Some src ->
     match eval_addressing genv sp addr rs##args with
                | Some a => (Mem.loadv chunk m a) = Some (rs # src)
@@ -426,8 +432,8 @@ Proof.
   
   {
     unfold sem_rel, sem_reg in REL.
-    generalize (PTree.elements_complete rel).
-    generalize (PTree.elements rel).
+    generalize (PTree.elements_complete (var_to_sym rel)).
+    generalize (PTree.elements (var_to_sym rel)).
     induction l; simpl.
     {
       intros.
@@ -454,7 +460,7 @@ Proof.
     destruct eq_args; trivial.
     subst args0.
     simpl.
-    assert ((rel ! r) = Some (SLoad chunk addr args)) as RELatr.
+    assert (((var_to_sym rel) ! r) = Some (SLoad chunk addr args)) as RELatr.
     {
       apply COMPLETE.
       left.
@@ -497,7 +503,7 @@ Proof.
   2: (apply IHargs; assumption).
   unfold forward_move, sem_rel, sem_reg, sem_sym_val in *.
   pose proof (REL a) as RELa.
-  destruct (rel ! a); trivial.
+  destruct (_ ! a); trivial.
   destruct s; congruence.
 Qed.
 
@@ -580,6 +586,7 @@ Proof.
   {
     subst x.
     unfold sem_reg.
+    simpl.
     rewrite PTree.gss.
     rewrite Regmap.gss.
     simpl.
@@ -588,6 +595,7 @@ Proof.
   }
   rewrite Regmap.gso by congruence.
   unfold sem_reg.
+  simpl.
   rewrite PTree.gso by congruence.
   rewrite Regmap.gso in KILL by congruence.
   exact KILL.
@@ -661,6 +669,7 @@ Proof.
   intros REL x.
   pose proof (REL x) as RELx.
   unfold kill_reg, sem_reg in *.
+  simpl.
   rewrite PTree.gfilter1.
   destruct (peq res x).
   { subst x.
@@ -668,7 +677,7 @@ Proof.
     reflexivity.
   }
   rewrite PTree.gro by congruence.
-  destruct (mpc ! x) as [sv | ]; trivial.
+  destruct (_ ! x) as [sv | ]; trivial.
   destruct negb; trivial.
 Qed.
 
@@ -691,8 +700,8 @@ Proof.
   pose proof (RE x) as REx.
   pose proof (GE x) as GEx.
   unfold sem_reg in *.
-  destruct (r1 ! x) as [r1x | ] in *;
-    destruct (r2 ! x) as [r2x | ] in *;
+  destruct ((var_to_sym r1) ! x) as [r1x | ] in *;
+    destruct ((var_to_sym r2) ! x) as [r2x | ] in *;
     congruence.
 Qed.
 End SAME_MEMORY.
@@ -708,9 +717,10 @@ Proof.
   intros SEM x.
   pose proof (SEM x) as SEMx.
   unfold kill_mem.
+  simpl.
   rewrite PTree.gfilter1.
   unfold kill_sym_val_mem.
-  destruct (rel ! x) as [ sv | ].
+  destruct ((var_to_sym rel) ! x) as [ sv | ].
   2: reflexivity.
   destruct sv; simpl in *; trivial.
   {