From f2426972df3fa959f09490b0b5752906d949c978 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 3 Apr 2019 11:00:46 +0200 Subject: We now generate load/store with 3 registers (ld rd rs1[rs2]), proofs admitted --- mppa_k1c/Asmblockgenproof1.v | 40 ++++++---------------------------------- 1 file changed, 6 insertions(+), 34 deletions(-) (limited to 'mppa_k1c/Asmblockgenproof1.v') 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, -- cgit