diff options
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 41 |
1 files changed, 19 insertions, 22 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 6cf5c60c..bbcffbe2 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -745,7 +745,7 @@ Proof. * constructor. * split; auto. simpl. intros. assert (rs r1 = (nextblock tbb rs) r1). - unfold nextblock. Simpl. rewrite H1 in H0. + unfold nextblock, incrPC. Simpl. rewrite H1 in H0. (*assert (Val.cmp_bool Ceq (rs r1) (Vint (Int.repr 0)) = Some b) as EVAL'S. { rewrite <- H2. rewrite <- H0. rewrite <- H1. auto. }*) auto; @@ -772,7 +772,7 @@ Proof. * constructor. * split; auto. simpl. intros. assert (rs r1 = (nextblock tbb rs) r1). - unfold nextblock. Simpl. rewrite H1 in H0. + unfold nextblock, incrPC. Simpl. rewrite H1 in H0. auto; unfold eval_branch. rewrite H0. auto. - (* c = Clt *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero); @@ -821,7 +821,7 @@ Proof. * constructor. * split; auto. simpl. intros. assert (rs r1 = (nextblock tbb rs) r1). - unfold nextblock. Simpl. rewrite H1 in H0. + unfold nextblock, incrPC. Simpl. rewrite H1 in H0. auto; unfold eval_branch. rewrite H0; auto. - (* c = Cne *) @@ -846,7 +846,7 @@ Proof. * constructor. * split; auto. simpl. intros. assert (rs r1 = (nextblock tbb rs) r1). - unfold nextblock. Simpl. rewrite H1 in H0. + unfold nextblock, incrPC. Simpl. rewrite H1 in H0. auto; unfold eval_branch. rewrite H0; auto. - (* c = Clt *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero); @@ -903,7 +903,7 @@ Proof. * constructor. * split; auto. assert (rs x = (nextblock tbb rs) x). - unfold nextblock. Simpl. rewrite H0 in EVAL'. clear H0. + unfold nextblock, incrPC. Simpl. rewrite H0 in EVAL'. clear H0. destruct c0; simpl; auto; unfold eval_branch; rewrite <- H; rewrite EVAL'; auto. + exploit (loadimm32_correct RTMP n); eauto. intros (rs' & A & B & C). @@ -966,7 +966,7 @@ Proof. * constructor. * split; auto. assert (rs x = (nextblock tbb rs) x). - unfold nextblock. Simpl. rewrite H0 in EVAL'. clear H0. + unfold nextblock, incrPC. Simpl. rewrite H0 in EVAL'. clear H0. destruct c0; simpl; auto; unfold eval_branch; rewrite <- H; rewrite EVAL'; auto. + exploit (loadimm64_correct RTMP n); eauto. intros (rs' & A & B & C). @@ -1060,13 +1060,10 @@ Lemma transl_cbranch_correct_false: /\ exec_control ge fn (Some insn) (nextblock tbb rs') m' = Next (nextblock tbb rs') m' /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. Proof. - intros. exploit transl_cbranch_correct_1; eauto. + intros. exploit transl_cbranch_correct_1. all: eauto. simpl eval_branch. instantiate (1 := tbb). + intros (rs' & insn & A & B & C). rewrite regset_same_assign in B. + eexists; eexists. split; try split. all: eassumption. Qed. -(* intros (rs' & insn & A & B & C). - exists rs'. - split. eapply exec_straight_opt_right; eauto. apply exec_straight_one; auto. - intros; Simpl. - *) (** Translation of condition operators *) @@ -1950,7 +1947,7 @@ Proof. intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C). econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. rewrite EXEC. - unfold exec_load_offset. rewrite PtrEq. rewrite B, LOAD. eauto. Simpl. + unfold exec_load_offset. unfold parexec_load_offset. rewrite PtrEq. rewrite B, LOAD. eauto. Simpl. split; intros; Simpl. auto. Qed. @@ -1970,7 +1967,7 @@ Proof. intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C). econstructor; split. eapply exec_straight_opt_right. eapply A. apply exec_straight_one. rewrite EXEC. - unfold exec_store_offset. rewrite PtrEq. rewrite B, C, STORE. + unfold exec_store_offset. unfold parexec_store_offset. rewrite PtrEq. rewrite B, C, STORE. eauto. discriminate. { intro. inv H. contradiction. } @@ -2149,7 +2146,7 @@ Proof. intros (base & ro2 & mro2 & mr2 & rs' & ARGSS & IREGEQ & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mr2 mro2. clear ARGS. econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2. - rewrite INSTR. unfold exec_load_reg. rewrite B, LOAD. reflexivity. Simpl. + rewrite INSTR. unfold exec_load_reg. unfold parexec_load_reg. rewrite B, LOAD. reflexivity. Simpl. split; intros; Simpl. auto. Qed. @@ -2170,7 +2167,7 @@ Proof. intros (base & ofs & rs' & ptr & A & PtrEq & B & C). econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. - rewrite INSTR. unfold exec_load_offset. rewrite PtrEq, B, LOAD. reflexivity. Simpl. + rewrite INSTR. unfold exec_load_offset. unfold parexec_load_offset. rewrite PtrEq, B, LOAD. reflexivity. Simpl. split; intros; Simpl. auto. Qed. @@ -2256,7 +2253,7 @@ Proof. intros (base & ro2 & mr2 & mro2 & rs' & ARGSS & IREGG & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mro2 mr2. clear ARGS. econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2. - rewrite INSTR. unfold exec_store_reg. rewrite B. rewrite C; try discriminate. rewrite STORE. auto. + rewrite INSTR. unfold exec_store_reg. unfold parexec_store_reg. rewrite B. rewrite C; try discriminate. rewrite STORE. auto. intro. inv H. contradiction. auto. Qed. @@ -2278,7 +2275,7 @@ Proof. intros (base & ofs & rs' & ptr & A & PtrEq & B & C). econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. - rewrite INSTR. unfold exec_store_offset. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto. + rewrite INSTR. unfold exec_store_offset. unfold parexec_store_offset. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto. intro. inv H. contradiction. auto. Qed. @@ -2287,14 +2284,14 @@ Qed. Remark exec_store_offset_8_sign rs m x base ofs: exec_store_offset ge Mint8unsigned rs m x base ofs = exec_store_offset ge Mint8signed rs m x base ofs. Proof. - unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev. + unfold exec_store_offset. unfold parexec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev. destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_8. reflexivity. Qed. Remark exec_store_offset_16_sign rs m x base ofs: exec_store_offset ge Mint16unsigned rs m x base ofs = exec_store_offset ge Mint16signed rs m x base ofs. Proof. - unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev. + unfold exec_store_offset. unfold parexec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev. destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_16. reflexivity. Qed. @@ -2336,14 +2333,14 @@ Qed. Remark exec_store_reg_8_sign rs m x base ofs: exec_store_reg Mint8unsigned rs m x base ofs = exec_store_reg Mint8signed rs m x base ofs. Proof. - unfold exec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto. + unfold exec_store_reg. unfold parexec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto. erewrite <- Mem.store_signed_unsigned_8. reflexivity. Qed. Remark exec_store_reg_16_sign rs m x base ofs: exec_store_reg Mint16unsigned rs m x base ofs = exec_store_reg Mint16signed rs m x base ofs. Proof. - unfold exec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto. + unfold exec_store_reg. unfold parexec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto. erewrite <- Mem.store_signed_unsigned_16. reflexivity. Qed. |