diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-10-10 17:35:40 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-10-10 17:35:40 +0200 |
| commit | 2adcf74ddf10ec2cf577238c73f3389469e72d41 (patch) | |
| tree | f968d56d5e1907c5d7ab7d0bfb9b26504a862bcb /mppa_k1c/Asmblockgenproof0.v | |
| parent | 83119fc0b190707cf5025ae2f44ac13dec68b692 (diff) | |
| download | compcert-kvx-2adcf74ddf10ec2cf577238c73f3389469e72d41.tar.gz compcert-kvx-2adcf74ddf10ec2cf577238c73f3389469e72d41.zip | |
Avancement du schéma. A voir problème des traces
Diffstat (limited to 'mppa_k1c/Asmblockgenproof0.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof0.v | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v index 81dd36b5..5c2d6f02 100644 --- a/mppa_k1c/Asmblockgenproof0.v +++ b/mppa_k1c/Asmblockgenproof0.v @@ -754,7 +754,7 @@ Proof. auto. Qed. -Lemma exec_straight_pc: +(* Lemma exec_straight_pc': forall c rs1 m1 rs2 m2, exec_straight c rs1 m1 nil rs2 m2 -> rs2 PC = rs1 PC. @@ -764,6 +764,18 @@ Proof. - erewrite exec_basic_instr_pc; eauto. - rewrite (IHc rs3 m3 rs2 m2); auto. erewrite exec_basic_instr_pc; eauto. +Qed. *) + +Lemma exec_straight_pc: + forall c c' rs1 m1 rs2 m2, + exec_straight c rs1 m1 c' rs2 m2 -> + rs2 PC = rs1 PC. +Proof. + induction c; intros; try (inv H; fail). + inv H. + - eapply exec_basic_instr_pc; eauto. + - rewrite (IHc c' rs3 m3 rs2 m2); auto. + erewrite exec_basic_instr_pc; eauto. Qed. Lemma exec_straight_through: @@ -777,11 +789,11 @@ Proof. intros. subst. destruct i. - constructor 1. + unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. - + rewrite <- (exec_straight_pc c rs1 m1 rs2 m2'); auto. + + rewrite <- (exec_straight_pc c nil rs1 m1 rs2 m2'); auto. - destruct c as [|i c]; try (inv H0; fail). constructor 1. + unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. - + rewrite <- (exec_straight_pc (i ::i c) rs1 m1 rs2 m2'); auto. + + rewrite <- (exec_straight_pc (i ::i c) nil rs1 m1 rs2 m2'); auto. Qed. Lemma exec_straight_through_singleinst: |