#91 Removed completely the duplicated semantics in Asmblock

1 files changed, 34 insertions, 34 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 32e5e5bb..a88a2dff 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -729,7 +729,7 @@ Lemma trans_arith_correct:
      inst_run (Genv ge fn) (trans_arith i) s s = Some s'
   /\ match_states (State rs' m) s'.
 Proof.
-  intros. unfold exec_arith_instr in H. destruct i.
+  intros. unfold exec_arith_instr in H. unfold parexec_arith_instr in H. destruct i.
 (* Ploadsymbol *)
   - inv H; inv H0. eexists; split; try split.
     * Simpl.
@@ -816,16 +816,16 @@ Theorem forward_simu_basic_gen ge fn b rs m s:
 Proof.
   intros. destruct b; inversion H; simpl.
 (* Arith *)
-  - eapply trans_arith_correct; eauto.
+  - eapply trans_arith_correct; eauto. destruct i; simpl; reflexivity.
 (* Load *)
   - destruct i.
   (* Load Offset *)
     + destruct i; simpl;
-      unfold exec_load_offset; rewrite (H1 ra); rewrite H0;
+      unfold parexec_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;
+      unfold parexec_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.
 
@@ -833,12 +833,12 @@ Proof.
   - destruct i.
   (* Store Offset *)
     + destruct i; simpl;
-      rewrite (H1 rs0); rewrite (H1 ra); rewrite H0; unfold exec_store_offset; destruct (eval_offset _ _); simpl; auto;
+      rewrite (H1 rs0); rewrite (H1 ra); rewrite H0; unfold parexec_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;
+      rewrite (H1 rs0); rewrite (H1 ra); rewrite (H1 rofs); rewrite H0; unfold parexec_store_reg; unfold exec_store_deps_reg;
       destruct (Mem.storev _ _ _ _); simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl.
 
 (* Allocframe *)
@@ -914,39 +914,39 @@ Proof.
 
     (* Pjumptable *)
     + Simpl. rewrite (H2 r). destruct (rs r); simpl; auto. destruct (list_nth_z _ _); simpl; auto.
-      unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
+      unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl.
       destruct (Val.offset_ptr _ _); simpl; auto.
       eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
       destruct (preg_eq GPR62 g). rewrite e. Simpl.
       destruct (preg_eq GPR63 g). rewrite e. Simpl. Simpl.
 
     (* Pj_l *)
-    + Simpl. unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto.
+    + Simpl. unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto.
       unfold nextblock. Simpl. destruct (Val.offset_ptr _ _); simpl; auto.
       eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
 
     (* Pcb *)
-    + Simpl. destruct (cmp_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold eval_branch; unfold eval_branch_deps.
+    + Simpl. destruct (cmp_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold par_eval_branch; unfold eval_branch_deps.
       ++ destruct (Val.cmp_bool _ _ _); simpl; auto. destruct b0.
-         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
+         +++ unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto.
              eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
          +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
       ++ destruct (Val.cmpl_bool _ _ _); simpl; auto. destruct b0.
-         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
+         +++ unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto.
              eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
          +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
 
     (* Pcbu *)
-    + Simpl. destruct (cmpu_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold eval_branch; unfold eval_branch_deps.
+    + Simpl. destruct (cmpu_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold par_eval_branch; unfold eval_branch_deps.
       ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b0.
-         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
+         +++ unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto.
              eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
          +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
       ++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b0.
-         +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
+         +++ unfold par_goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl.
              destruct (Val.offset_ptr _ _); simpl; auto.
              eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
          +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl.
@@ -1090,41 +1090,41 @@ Proof.
 (* Pjumptable *)
   - simpl in *. repeat (rewrite H3 in H1).
     destruct (rs r); try discriminate; auto. destruct (list_nth_z _ _); try discriminate; auto.
-    unfold goto_label_deps in H1. unfold goto_label. Simpl.
+    unfold goto_label_deps in H1. unfold par_goto_label. Simpl.
     destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
 (* Pj_l *)
   - simpl in *. pose (H3 PC); simpl in e; rewrite e in H1. clear e.
-    unfold goto_label_deps in H1. unfold goto_label.
+    unfold goto_label_deps in H1. unfold par_goto_label.
     destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
 (* Pcb *)
   - simpl in *. destruct (cmp_for_btest bt). destruct i.
     + pose (H3 PC); simpl in e; rewrite e in H1; clear e.
       destruct o; auto. pose (H3 r); simpl in e; rewrite e in H1; clear e.
-      unfold eval_branch_deps in H1; unfold eval_branch.
+      unfold eval_branch_deps in H1; unfold par_eval_branch.
       destruct (Val.cmp_bool _ _ _); auto. destruct b; try discriminate.
-      unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
+      unfold goto_label_deps in H1; unfold par_goto_label. destruct (label_pos _ _ _); auto.
       destruct (rs PC); auto. discriminate.
     + pose (H3 PC); simpl in e; rewrite e in H1; clear e.
       destruct o; auto. pose (H3 r); simpl in e; rewrite e in H1; clear e.
-      unfold eval_branch_deps in H1; unfold eval_branch.
+      unfold eval_branch_deps in H1; unfold par_eval_branch.
       destruct (Val.cmpl_bool _ _ _); auto. destruct b; try discriminate.
-      unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
+      unfold goto_label_deps in H1; unfold par_goto_label. destruct (label_pos _ _ _); auto.
       destruct (rs PC); auto. discriminate.
 (* Pcbu *)
   - simpl in *. destruct (cmpu_for_btest bt). destruct i.
     + pose (H3 PC); simpl in e; rewrite e in H1; clear e.
       destruct o; auto.
       pose (H3 r); simpl in e; rewrite e in H1; clear e.
-      unfold eval_branch_deps in H1; unfold eval_branch.
+      unfold eval_branch_deps in H1; unfold par_eval_branch.
       destruct (Val_cmpu_bool _ _ _); auto. destruct b; try discriminate.
-      unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
+      unfold goto_label_deps in H1; unfold par_goto_label. destruct (label_pos _ _ _); auto.
       destruct (rs PC); auto. discriminate.
     + pose (H3 PC); simpl in e; rewrite e in H1; clear e.
       destruct o; auto.
       pose (H3 r); simpl in e; rewrite e in H1; clear e.
-      unfold eval_branch_deps in H1; unfold eval_branch.
+      unfold eval_branch_deps in H1; unfold par_eval_branch.
       destruct (Val_cmplu_bool _ _); auto. destruct b; try discriminate.
-      unfold goto_label_deps in H1; unfold goto_label. destruct (label_pos _ _ _); auto.
+      unfold goto_label_deps in H1; unfold par_goto_label. destruct (label_pos _ _ _); auto.
       destruct (rs PC); auto. discriminate.
 Qed.
 
@@ -1173,37 +1173,37 @@ Proof.
   destruct ctl; destruct i; try discriminate; try (simpl; reflexivity).
   (* Pjumptable *)
   - simpl in *. repeat (rewrite H3). destruct (rs r); try discriminate; auto. destruct (list_nth_z _ _); try discriminate; auto.
-    unfold goto_label_deps. unfold goto_label in H0.
+    unfold goto_label_deps. unfold par_goto_label in H0.
     destruct (label_pos _ _ _); auto. repeat (rewrite Pregmap.gso in H0; try discriminate). destruct (rs PC); auto. discriminate.
 (* Pj_l *)
-  - simpl in *. pose (H3 PC); simpl in e; rewrite e. unfold goto_label_deps. unfold goto_label in H0.
+  - simpl in *. pose (H3 PC); simpl in e; rewrite e. unfold goto_label_deps. unfold par_goto_label in H0.
     destruct (label_pos _ _ _); auto. clear e. destruct (rs PC); auto. discriminate.
 (* Pcb *)
   - simpl in *. destruct (cmp_for_btest bt). destruct i.
     -- destruct o.
-      + unfold eval_branch in H0; unfold eval_branch_deps.
+      + unfold par_eval_branch in H0; unfold eval_branch_deps.
         pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmp_bool _ _ _); auto.
-        destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
+        destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. clear e0.
         destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
       + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
     -- destruct o.
-      + unfold eval_branch in H0; unfold eval_branch_deps.
+      + unfold par_eval_branch in H0; unfold eval_branch_deps.
         pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val.cmpl_bool _ _ _); auto.
-        destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
+        destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. clear e0.
         destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
       + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
 (* Pcbu *)
   - simpl in *. destruct (cmpu_for_btest bt). destruct i.
     -- destruct o.
-      + unfold eval_branch in H0; unfold eval_branch_deps.
+      + unfold par_eval_branch in H0; unfold eval_branch_deps.
         pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val_cmpu_bool _ _); auto.
-        destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
+        destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. clear e0.
         destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
       + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
     -- destruct o.
-      + unfold eval_branch in H0; unfold eval_branch_deps.
+      + unfold par_eval_branch in H0; unfold eval_branch_deps.
         pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. destruct (Val_cmplu_bool _ _); auto.
-        destruct b; try discriminate. unfold goto_label_deps; unfold goto_label in H0. clear e0.
+        destruct b; try discriminate. unfold goto_label_deps; unfold par_goto_label in H0. clear e0.
         destruct (label_pos _ _ _); auto. destruct (rs PC); auto. discriminate.
       + pose (H3 r); simpl in e; rewrite e. pose (H3 PC); simpl in e0; rewrite e0. reflexivity.
 Qed.