Refactorisation de forward_simu_basic

1 files changed, 55 insertions, 102 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index a5880128..92630772 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -810,80 +810,78 @@ Proof.
       destruct (ireg_eq g rd); subst; Simpl.
 Qed.
 
-Lemma forward_simu_basic:
-  forall ge fn b rs m rs' m' s,
-  exec_basic_instr ge b rs m = Next rs' m' ->
+Theorem forward_simu_basic_gen ge fn b rs m s:
   match_states (State rs m) s ->
-  exists s',
-     inst_run (Genv ge fn) (trans_basic b) s s = Some s'
-  /\ match_states (State rs' m') s'.
+  match_outcome (exec_basic_instr ge b rs m) (inst_run (Genv ge fn) (trans_basic b) s s).
 Proof.
-  intros. destruct b.
+  intros. destruct b; inversion H; simpl.
 (* Arith *)
-  - simpl in H. inv H. simpl inst_run. eapply trans_arith_correct; eauto.
+  - eapply trans_arith_correct; eauto.
 (* Load *)
-  - simpl in H. destruct i.
+  - destruct i.
   (* Load Offset *)
-    + destruct i. all:
-      unfold exec_load_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate;
-      destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
-      eexists; split; try split; [
-        simpl; rewrite EVALOFF; rewrite H; rewrite (H1 ra); simpl in MEML; rewrite MEML; reflexivity
-      | Simpl
-      | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ].
-  (* Load Reg *)
-    + destruct i. all:
-      unfold exec_load_reg in H; destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
-      eexists; split; try split;
-      [ simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); unfold exec_load_deps_reg; simpl in MEML; rewrite MEML; reflexivity
-      | Simpl
-      | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ].
+    + destruct i; simpl;
+      unfold exec_load_offset; rewrite (H1 ra); rewrite H0;
+      destruct (eval_offset _ _); simpl; auto; destruct (Mem.loadv _ _); simpl; auto;
+      eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
+    + destruct i; simpl;
+      unfold exec_load_reg; rewrite (H1 ra); rewrite (H1 rofs); rewrite H0; unfold exec_load_deps_reg;
+      destruct (Mem.loadv _ _); simpl; auto;
+      eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
 
 (* Store *)
-  - simpl in H. destruct i.
+  - destruct i.
   (* Store Offset *)
-    + destruct i. all:
-      unfold exec_store_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate;
-      destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
-      eexists; split; try split;
-      [ simpl; rewrite EVALOFF; rewrite H; rewrite (H1 ra); rewrite (H1 rs0); simpl in MEML; rewrite MEML; reflexivity
-      | Simpl
-      | intros rr; destruct rr; Simpl ].
-  (* Store Reg *)
-    + destruct i. all:
-      unfold exec_store_reg in H;
-      destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
-      eexists; split; try split;
-      [ simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); rewrite (H1 rs0); unfold exec_store_deps_reg;
-        simpl in MEML; rewrite MEML; reflexivity
-      | Simpl
-      | intros rr; destruct rr; Simpl ].
+    + destruct i; simpl;
+      rewrite (H1 rs0); rewrite (H1 ra); rewrite H0; unfold exec_store_offset; destruct (eval_offset _ _); simpl; auto;
+      destruct (Mem.storev _ _ _ _); simpl; auto;
+      eexists; split; try split; Simpl; intros rr; destruct rr; Simpl.
+
+    + destruct i; simpl;
+      rewrite (H1 rs0); rewrite (H1 ra); rewrite (H1 rofs); rewrite H0; unfold exec_store_reg; unfold exec_store_deps_reg;
+      destruct (Mem.storev _ _ _ _); simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl.
 
 (* Allocframe *)
-  - simpl in H. destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS; try discriminate.
-    inv H. inv H0. eexists. split; try split.
-    * simpl. Simpl. pose (H1 GPR12); simpl in e; rewrite e. rewrite H. rewrite MEMAL. rewrite MEMS. Simpl.
-      rewrite H. rewrite MEMAL. rewrite MEMS. reflexivity.
+  - Simpl. rewrite (H1 SP). rewrite H0. destruct (Mem.alloc _ _ _) eqn:ALLOC; simpl; auto. destruct (Mem.store _ _ _ _) eqn:STORE; simpl; auto.
+    eexists; split; try split.
+    * Simpl. rewrite H0. rewrite ALLOC. rewrite STORE. reflexivity.
     * Simpl.
-    * intros rr; destruct rr; Simpl.
-      destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl.
+    * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl.
+
 (* Freeframe *)
-  - simpl in H. destruct (Mem.loadv _ _ _) eqn:MLOAD; try discriminate. destruct (rs GPR12) eqn:SPeq; try discriminate.
-    destruct (Mem.free _ _ _ _) eqn:MFREE; try discriminate. inv H. inv H0.
-    eexists. split; try split.
-    * simpl. pose (H1 GPR12); simpl in e; rewrite e. rewrite H. rewrite SPeq. rewrite MLOAD. rewrite MFREE.
-      Simpl. rewrite e. rewrite SPeq. rewrite MLOAD. rewrite MFREE. reflexivity.
+  - rewrite (H1 SP). rewrite H0. destruct (Mem.loadv _ _ _) eqn:LOAD; simpl; auto. destruct (rs GPR12) eqn:SPeq; simpl; auto.
+    destruct (Mem.free _ _ _ _) eqn:FREE; simpl; auto. Simpl. rewrite (H1 SP). eexists; split; try split.
+    * rewrite SPeq. rewrite LOAD. rewrite FREE. reflexivity.
     * Simpl.
     * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g FP)]]; subst; Simpl.
+
 (* Pget *)
-  - simpl in H. destruct rs0 eqn:rs0eq; try discriminate. inv H. inv H0.
-    eexists. split; try split. Simpl. intros rr; destruct rr; Simpl.
-    destruct (ireg_eq g rd); subst; Simpl.
+  - destruct rs0; simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl.
+
 (* Pset *)
-  - simpl in H. destruct rd eqn:rdeq; try discriminate. inv H. inv H0.
-    eexists. split; try split. Simpl. intros rr; destruct rr; Simpl.
+  - destruct rd; simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
+
 (* Pnop *)
-  - simpl in H. inv H. inv H0. eexists. split; try split. assumption. assumption. 
+  - eexists; split; try split. assumption. assumption. 
+Qed.
+
+Lemma forward_simu_basic ge fn b rs m rs' m' s:
+  exec_basic_instr ge b rs m = Next rs' m' ->
+  match_states (State rs m) s ->
+  exists s',
+     inst_run (Genv ge fn) (trans_basic b) s s = Some s'
+  /\ match_states (State rs' m') s'.
+Proof.
+  intros. exploit forward_simu_basic_gen; eauto. intros. rewrite H in H1. inv H1. eexists. eassumption.
+Qed.
+
+Lemma forward_simu_basic_instr_stuck i ge fn rs m s:
+  Ge = Genv ge fn ->
+  exec_basic_instr ge i rs m = Stuck ->
+  match_states (State rs m) s ->
+  exec Ge [trans_basic i] s = None.
+Proof.
+  intros. exploit forward_simu_basic_gen; eauto. intros. rewrite H0 in H2. inv H2. unfold exec. unfold run. rewrite H4. reflexivity.
 Qed.
 
 Lemma forward_simu_body:
@@ -1147,51 +1145,6 @@ Proof.
   - left. reflexivity.
 Qed.
 
-Lemma forward_simu_basic_instr_stuck:
-  forall i ge fn rs m s,
-  Ge = Genv ge fn ->
-  exec_basic_instr ge i rs m = Stuck ->
-  match_states (State rs m) s ->
-  exec Ge [trans_basic i] s = None.
-Proof.
-  intros. inv H1. unfold exec_basic_instr in H0. destruct i; try discriminate.
-(* PLoad *)
-  - destruct i.
-  (* Load Offset *)
-    + destruct i. all:
-    simpl; rewrite H2; rewrite (H3 ra); unfold exec_load_offset in H0; destruct (eval_offset _ _); auto;
-    simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate.
-  (* Load Reg *)
-    + destruct i. all:
-    simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); unfold exec_load_reg in H0; unfold exec_load_deps_reg;
-    destruct (rs rofs); auto; simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate.
-
-(* PStore *)
-  - destruct i.
-  (* Store Offset *)
-    + destruct i. all:
-    simpl; rewrite H2; rewrite (H3 ra); rewrite (H3 rs0); unfold exec_store_offset in H0; destruct (eval_offset _ _); auto;
-    simpl in H0; destruct (Mem.storev _ _ _); auto; discriminate.
-  (* Store Reg *)
-    + destruct i. all:
-    simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); rewrite (H3 rs0); simpl in H0; unfold exec_store_reg in H0;
-    unfold exec_store_deps_reg; destruct (rs rofs); auto;
-    destruct (Mem.storev _ _ _ _); auto; discriminate.
-
-(* Pallocframe *)
-  - simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2. destruct (Mem.alloc _ _ _). simpl in H0.
-    destruct (Mem.store _ _ _ _); try discriminate. reflexivity.
-(* Pfreeframe *)
-  - simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2.
-    destruct (Mem.loadv _ _ _); auto. destruct (rs GPR12); auto. destruct (Mem.free _ _ _ _); auto.
-    discriminate.
-(* Pget *)
-  - simpl. destruct rs0; subst; try discriminate.
-    all: simpl; auto.
-  - simpl. destruct rd; subst; try discriminate.
-    all: simpl; auto.
-Qed.
-
 Lemma forward_simu_body_stuck:
   forall bdy ge fn rs m s,
   Ge = Genv ge fn ->