We now generate load/store with 3 registers (ld rd rs1[rs2]), proofs admitted

1 files changed, 6 insertions, 34 deletions

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index f8bbf7f4..06c9fb3e 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -30,40 +30,13 @@ Lemma make_immed32_sound:
 Proof.
   intros; unfold make_immed32. set (lo := Int.sign_ext 12 n).
   predSpec Int.eq Int.eq_spec n lo; auto.
-(*
-- auto.
-- set (m := Int.sub n lo).
-  assert (A: Int.eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto).
-  assert (B: Int.eqmod (two_p 12) (Int.unsigned n - Int.unsigned  lo) 0).
-  { replace 0 with (Int.unsigned n - Int.unsigned n) by omega.
-    auto using Int.eqmod_sub, Int.eqmod_refl. }
-  assert (C: Int.eqmod (two_p 12) (Int.unsigned m) 0).
-  { apply Int.eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto.
-    apply Int.eqmod_divides with Int.modulus. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
-    exists (two_p (32-12)); auto. }
-  assert (D: Int.modu m (Int.repr 4096) = Int.zero).
-  { apply Int.eqmod_mod_eq in C. unfold Int.modu. 
-    change (Int.unsigned (Int.repr 4096)) with (two_p 12). rewrite C. 
-    reflexivity.
-    apply two_p_gt_ZERO; omega. }
-  rewrite <- (Int.divu_pow2 m (Int.repr 4096) (Int.repr 12)) by auto.
-  rewrite Int.shl_mul_two_p. 
-  change (two_p (Int.unsigned (Int.repr 12))) with 4096.
-  replace (Int.mul (Int.divu m (Int.repr 4096)) (Int.repr 4096)) with m.
-  unfold m. rewrite Int.sub_add_opp. rewrite Int.add_assoc. rewrite <- (Int.add_commut lo).
-  rewrite Int.add_neg_zero. rewrite Int.add_zero. auto.
-  rewrite (Int.modu_divu_Euclid m (Int.repr 4096)) at 1 by (vm_compute; congruence).
-  rewrite D. apply Int.add_zero.
-*)
 Qed.
 
 Lemma make_immed64_sound:
   forall n,
   match make_immed64 n with
   | Imm64_single imm => n = imm
-(*| Imm64_pair hi lo => n = Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo
-  | Imm64_large imm => n = imm
-*)end.
+  end.
 Proof.
   intros; unfold make_immed64. set (lo := Int64.sign_ext 12 n).
   predSpec Int64.eq Int64.eq_spec n lo.
@@ -76,7 +49,6 @@ Proof.
 Qed.
 
 
-
 (** Properties of registers *)
 
 Lemma ireg_of_not_RTMP:
@@ -2000,10 +1972,10 @@ Proof.
    /\ transl_memory_access mk_instr addr args k = OK c
    /\ forall base ofs rs,
         exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs).
-  { unfold transl_load in TR; destruct chunk; ArgsInv; econstructor; (esplit; eauto). }
+  { (* unfold transl_load in TR; destruct chunk; ArgsInv; econstructor; (esplit; eauto). *) admit. }
   destruct A as (mk_instr & rd & rdEq & B & C). rewrite rdEq.
   eapply transl_load_access_correct; eauto with asmgen.
-Qed.
+Admitted.
 
 Lemma transl_store_correct:
   forall chunk addr args src k c (rs: regset) m a m',
@@ -2021,16 +1993,16 @@ Proof.
    /\ (forall base ofs rs,
         exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk' rs m rr base ofs)
    /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src)).
-  { unfold transl_store in TR; destruct chunk; ArgsInv;
+  { admit. (* unfold transl_store in TR; destruct chunk; ArgsInv;
     (econstructor; econstructor; econstructor; split; [eauto | split; [eassumption | split; [ intros; simpl; reflexivity | auto]]]).
     destruct a; auto. apply Mem.store_signed_unsigned_8. 
-    destruct a; auto. apply Mem.store_signed_unsigned_16. 
+    destruct a; auto. apply Mem.store_signed_unsigned_16.  *)
   }
   destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D).
   rewrite D in STORE; clear D. 
   eapply transl_store_access_correct; eauto with asmgen. congruence.
   destruct rr; try discriminate. destruct src; try discriminate.
-Qed.
+Admitted.
 
 Lemma make_epilogue_correct:
   forall ge0 f m stk soff cs m' ms rs k tm,