#91 Removed completely the duplicated semantics in Asmblock

6 files changed, 89 insertions, 257 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 3bcb321d..c7528272 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -39,113 +39,21 @@ Section RELSEM.
 
 Variable ge: genv.
 
-
-Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
-  match ai with
-  | PArithR n d => rs#d <- (arith_eval_r ge n)
-
-  | PArithRR n d s => rs#d <- (arith_eval_rr n rs#s)
-
-  | PArithRI32 n d i => rs#d <- (arith_eval_ri32 n i)
-  | PArithRI64 n d i => rs#d <- (arith_eval_ri64 n i)
-  | PArithRF32 n d i => rs#d <- (arith_eval_rf32 n i)
-  | PArithRF64 n d i => rs#d <- (arith_eval_rf64 n i)
-
-  | PArithRRR n d s1 s2 => rs#d <- (arith_eval_rrr n rs#s1 rs#s2)
-
-  | PArithRRI32 n d s i => rs#d <- (arith_eval_rri32 n rs#s i)
-
-  | PArithRRI64 n d s i => rs#d <- (arith_eval_rri64 n rs#s i)
-
-  | PArithARRR n d s1 s2 => rs#d <- (arith_eval_arrr n rs#d rs#s1 rs#s2)
-
-  | PArithARRI32 n d s i => rs#d <- (arith_eval_arri32 n rs#d rs#s i)
-
-  | PArithARRI64 n d s i => rs#d <- (arith_eval_arri64 n rs#d rs#s i)
-  end.
-
-(** * load/store *)
+Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := parexec_arith_instr ge ai rs rs.
 
 (** Auxiliaries for memory accesses *)
 
+Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := parexec_load_offset ge chunk rs rs m m d a ofs.
 
-Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) :=
-  match (eval_offset ge ofs) with
-  | OK ptr => match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with
-              | None => Stuck
-              | Some v => Next (rs#d <- v) m
-              end
-  | _ => Stuck
-  end.
-
-Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) :=
-  match Mem.loadv chunk m (Val.addl (rs a) (rs ro)) with
-  | None => Stuck
-  | Some v => Next (rs#d <- v) m
-  end.
-
-Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) :=
-  match (eval_offset ge ofs) with
-  | OK ptr => match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with
-              | None => Stuck
-              | Some m' => Next rs m'
-              end
-  | _ => Stuck
-  end.
-
-Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) :=
-  match Mem.storev chunk m (Val.addl (rs a) (rs ro)) (rs s) with
-  | None => Stuck
-  | Some m' => Next rs m'
-  end.
+Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_reg chunk rs rs m m d a ro.
 
+Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := parexec_store_offset ge chunk rs rs m m s a ofs.
 
+Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_reg chunk rs rs m m s a ro.
 
 (** * basic instructions *)
 
-Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome :=
-  match bi with
-  | PArith ai => Next (exec_arith_instr ai rs) m
-
-  | PLoadRRO n d a ofs => exec_load_offset (load_chunk n) rs m d a ofs
-  | PLoadRRR n d a ro => exec_load_reg (load_chunk n) rs m d a ro
-
-  | PStoreRRO n s a ofs => exec_store_offset (store_chunk n) rs m s a ofs
-  | PStoreRRR n s a ro => exec_store_reg (store_chunk n) rs m s a ro
-
-  | Pallocframe sz pos =>
-      let (m1, stk) := Mem.alloc m 0 sz in
-      let sp := (Vptr stk Ptrofs.zero) in
-      match Mem.storev Mptr m1 (Val.offset_ptr sp pos) rs#SP with
-      | None => Stuck
-      | Some m2 => Next (rs #FP <- (rs SP) #SP <- sp #RTMP <- Vundef) m2
-      end
-
-  | Pfreeframe sz pos =>
-      match Mem.loadv Mptr m (Val.offset_ptr rs#SP pos) with
-      | None => Stuck
-      | Some v =>
-          match rs SP with
-          | Vptr stk ofs =>
-              match Mem.free m stk 0 sz with
-              | None => Stuck
-              | Some m' => Next (rs#SP <- v #RTMP <- Vundef) m'
-              end
-          | _ => Stuck
-          end
-      end
-  | Pget rd ra =>
-    match ra with
-    | RA => Next (rs#rd <- (rs#ra)) m
-    | _  => Stuck
-    end
-  | Pset ra rd =>
-    match ra with
-    | RA => Next (rs#ra <- (rs#rd)) m
-    | _  => Stuck
-    end
-  | Pnop => Next rs m
-end.
+Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := parexec_basic_instr ge bi rs rs m m.
 
 Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
   match body with
@@ -157,34 +65,16 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
      end
   end.
 
-
-
 (** Position corresponding to a label *)
 
-
-
-Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome :=
-  match label_pos lbl 0 (fn_blocks f) with
-  | None => Stuck
-  | Some pos =>
-      match rs#PC with
-      | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m
-      | _          => Stuck
-      end
-  end.
+Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome := par_goto_label f lbl rs rs m.
 
 (** Evaluating a branch 
 
 Warning: in m PC is assumed to be already pointing on the next instruction !
 
 *)
-Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome :=
-  match res with
-    | Some true  => goto_label f l rs m
-    | Some false => Next rs m
-    | None => Stuck
-  end.
-
+Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome := par_eval_branch f l rs rs m res.
 
 (** Execution of a single control-flow instruction [i] in initial state [rs] and
     [m].  Return updated state.
@@ -202,55 +92,7 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti
     we generate cannot use those registers to hold values that must
     survive the execution of the pseudo-instruction. *)
 
-Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome :=
-  match oc with
-  | Some ic =>
-(** Get/Set system registers *)
-  match ic with
-
-
-(** Branch Control Unit instructions *)
-  | Pret =>
-      Next (rs#PC <- (rs#RA)) m
-  | Pcall s =>
-      Next (rs#RA <- (rs#PC) #PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
-  | Picall r =>
-      Next (rs#RA <- (rs#PC) #PC <- (rs#r)) m
-  | Pgoto s =>
-      Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
-  | Pigoto r =>
-      Next (rs#PC <- (rs#r)) m
-  | Pj_l l =>
-      goto_label f l rs m
-  | Pjumptable r tbl =>
-      match rs#r with
-      | Vint n =>
-          match list_nth_z tbl (Int.unsigned n) with
-          | None => Stuck
-          | Some lbl => goto_label f lbl (rs #GPR62 <- Vundef #GPR63 <- Vundef) m
-          end
-      | _ => Stuck
-      end
-      
-  | Pcb bt r l =>
-      match cmp_for_btest bt with
-      | (Some c, Int)  => eval_branch f l rs m (Val.cmp_bool c rs#r (Vint (Int.repr 0)))
-      | (Some c, Long) => eval_branch f l rs m (Val.cmpl_bool c rs#r (Vlong (Int64.repr 0)))
-      | (None, _) => Stuck
-      end
-  | Pcbu bt r l => 
-      match cmpu_for_btest bt with
-      | (Some c, Int) => eval_branch f l rs m (Val_cmpu_bool c rs#r (Vint (Int.repr 0)))
-      | (Some c, Long) => eval_branch f l rs m (Val_cmplu_bool c rs#r (Vlong (Int64.repr 0)))
-      | (None, _) => Stuck
-      end
-
-(** Pseudo-instructions *)
-  | Pbuiltin ef args res =>
-      Stuck (**r treated specially below *)
-  end
-  | None => Next rs m
-end.
+Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome := parexec_control ge f oc rs rs m.
 
 Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome :=
   match exec_body (body b) rs0 m with
@@ -259,19 +101,6 @@ Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcom
   | Stuck => Stuck
   end.
 
-(** Translation of the LTL/Linear/Mach view of machine registers to
-  the RISC-V view.  Note that no LTL register maps to [X31].  This
-  register is reserved as temporary, to be used by the generated RV32G
-  code.  *)
-
-
-
-
-
-
-
-(** Execution of the instruction at [rs PC]. *)
-
 
 (** TODO
  * For now, we consider a builtin is alone in a basic block.
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.
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index a071a9f8..1fbe7832 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -259,7 +259,7 @@ Proof.
   exploit label_pos_code_tail; eauto. instantiate (1 := 0).

   intros [pos' [P [Q R]]].

   exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))).

-  split. unfold goto_label. rewrite P. rewrite H1. auto.

+  split. unfold goto_label. unfold par_goto_label. rewrite P. rewrite H1. auto.

   split. rewrite Pregmap.gss. constructor; auto.

   rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.

   auto. omega.

@@ -1680,7 +1680,7 @@ Proof.
   { change (fn_blocks tf) with tfbody; unfold tfbody.

     apply exec_straight_blocks_step with rs2 m2'.

     unfold exec_bblock. simpl exec_body. rewrite C. fold sp. simpl exec_control.

-    rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. reflexivity.

+    rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. rewrite regset_same_assign. reflexivity.

     reflexivity.

     eapply exec_straight_blocks_trans.

     - eexact W'.

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 5ccea246..d44b033c 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -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 *)
 
@@ -1749,7 +1746,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.
 
@@ -1769,7 +1766,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. }
@@ -1948,7 +1945,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.
 
@@ -1969,7 +1966,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.
 
@@ -2055,7 +2052,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.
@@ -2077,7 +2074,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.
@@ -2086,14 +2083,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.
 
@@ -2135,14 +2132,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.
 
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 599a4024..a2dd2ec2 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -100,7 +100,7 @@ Lemma exec_load_offset_pc_var:
   exec_load_offset ge t rs m rd ra ofs = Next rs' m' ->
   exec_load_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
+  intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
   destruct (Mem.loadv _ _ _).
   - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
   - discriminate.
@@ -111,7 +111,7 @@ Lemma exec_load_reg_pc_var:
   exec_load_reg t rs m rd ra ro = Next rs' m' ->
   exec_load_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_load_reg in *. rewrite Pregmap.gso; try discriminate.
+  intros. unfold exec_load_reg in *. unfold parexec_load_reg in *. rewrite Pregmap.gso; try discriminate.
   destruct (Mem.loadv _ _ _).
   - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
   - discriminate.
@@ -122,7 +122,7 @@ Lemma exec_store_offset_pc_var:
   exec_store_offset ge t rs m rd ra ofs = Next rs' m' ->
   exec_store_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_store_offset in *. rewrite Pregmap.gso; try discriminate.
+  intros. unfold exec_store_offset in *. unfold parexec_store_offset in *. rewrite Pregmap.gso; try discriminate.
   destruct (eval_offset ge ofs); try discriminate.
   destruct (Mem.storev _ _ _).
   - inv H. apply next_eq; auto.
@@ -134,7 +134,7 @@ Lemma exec_store_reg_pc_var:
   exec_store_reg t rs m rd ra ro = Next rs' m' ->
   exec_store_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_store_reg in *. rewrite Pregmap.gso; try discriminate.
+  intros. unfold exec_store_reg in *. unfold parexec_store_reg in *. rewrite Pregmap.gso; try discriminate.
   destruct (Mem.storev _ _ _).
   - inv H. apply next_eq; auto.
   - discriminate.
@@ -145,13 +145,13 @@ Lemma exec_basic_instr_pc_var:
   exec_basic_instr ge i rs m = Next rs' m' ->
   exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.
 Proof.
-  intros. unfold exec_basic_instr in *. destruct i.
+  intros. unfold exec_basic_instr in *. unfold parexec_basic_instr in *. destruct i.
   - unfold exec_arith_instr in *. destruct i; destruct i.
       all: try (exploreInst; inv H; apply next_eq; auto;
       apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
-
+(* 
       (* Some cases treated seperately because exploreInst destructs too much *)
-      all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
+      all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). *)
   - destruct i.
     + exploreInst; apply exec_load_offset_pc_var; auto.
     + exploreInst; apply exec_load_reg_pc_var; auto.
@@ -223,10 +223,11 @@ Proof.
   exploit concat2_decomp; eauto. intros. inv H.
   unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate.
   rewrite H0 in EXEB'. apply exec_body_app in EXEB'. destruct EXEB' as (rs1 & m1 & EXEB1 & EXEB2).
-  repeat eexists.
+  eexists; eexists. split.
     unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto.
+  split.
     exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto.
-    unfold exec_bblock. unfold nextblock. erewrite exec_body_pc_var; eauto.
+    unfold exec_bblock. unfold nextblock. rewrite regset_same_assign. erewrite exec_body_pc_var; eauto.
     rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id.
     assert (size bb = size a + size b).
     { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r.
@@ -571,13 +572,8 @@ Proof.
   assert (ge = Genv.globalenv prog). auto.
   assert (tge = Genv.globalenv tprog). auto.
   pose symbol_address_preserved.
-  exploreInst; simpl; auto; try congruence.
-  - unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
-  - unfold eval_branch. unfold goto_label. erewrite label_pos_preserved_blocks; eauto.
+  exploreInst; simpl; auto; try congruence;
+    unfold par_goto_label; unfold par_eval_branch; unfold par_goto_label; erewrite label_pos_preserved_blocks; eauto.
 Qed.
 
 Lemma eval_offset_preserved:
@@ -589,21 +585,21 @@ Qed.
 Lemma transf_exec_load_offset:
   forall t rs m rd ra ofs, exec_load_offset ge t rs m rd ra ofs = exec_load_offset tge t rs m rd ra ofs.
 Proof.
-  intros. unfold exec_load_offset. rewrite eval_offset_preserved. reflexivity.
+  intros. unfold exec_load_offset. unfold parexec_load_offset. rewrite eval_offset_preserved. reflexivity.
 Qed.
 
 Lemma transf_exec_store_offset:
   forall t rs m rs0 ra ofs, exec_store_offset ge t rs m rs0 ra ofs = exec_store_offset tge t rs m rs0 ra ofs.
 Proof.
-  intros. unfold exec_store_offset. rewrite eval_offset_preserved. reflexivity.
+  intros. unfold exec_store_offset. unfold parexec_store_offset. rewrite eval_offset_preserved. reflexivity.
 Qed.
 
 Lemma transf_exec_basic_instr:
   forall i rs m, exec_basic_instr ge i rs m = exec_basic_instr tge i rs m.
 Proof.
   intros. pose symbol_address_preserved.
-  unfold exec_basic_instr. exploreInst; simpl; auto; try congruence.
-  - unfold exec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence.
+  unfold exec_basic_instr. unfold parexec_basic_instr. exploreInst; simpl; auto; try congruence.
+  - unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence.
   - apply transf_exec_load_offset.
   - apply transf_exec_store_offset.
 Qed.
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index 8a83521c..a44c40d8 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -14,6 +14,7 @@ Require Import Machblock.
 Require Import Asmblock.
 Require Import Asmblockgen.
 Require Import Conventions1.
+Require Import Axioms.
 
 Module MB:=Machblock.
 Module AB:=Asmvliw.
@@ -943,10 +944,10 @@ Lemma exec_basic_instr_pc:
 Proof.
   intros. destruct b; try destruct i; try destruct i.
   all: try (inv H; Simpl).
-  1-10: try (unfold exec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
-  1-10: try (unfold exec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
-  1-10: try (unfold exec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]).
-  1-10: try (unfold exec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
+  1-10: try (unfold parexec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
+  1-10: try (unfold parexec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
+  1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]).
+  1-10: try (unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
   - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
   - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
     destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.
@@ -997,6 +998,13 @@ Proof.
     + rewrite <- (exec_straight_pc (i ::i c) nil rs1 m1 rs2 m2'); auto.
 Qed.
  *)
+
+Lemma regset_same_assign (rs: regset) r:
+  rs # r <- (rs r) = rs.
+Proof.
+  apply functional_extensionality. intros x. destruct (preg_eq x r); subst; Simpl.
+Qed.
+
 Lemma exec_straight_through_singleinst:
   forall a b rs1 m1 rs2 m2 rs2' m2' lb,
   bblock_single_inst (PBasic a) = b ->
@@ -1005,10 +1013,12 @@ Lemma exec_straight_through_singleinst:
   exec_straight_blocks (b::lb) rs1 m1 lb rs2' m2'.
 Proof.
   intros. subst. constructor 1. unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto.
-  simpl. auto.
+  simpl. rewrite regset_same_assign. auto.
   simpl; auto. unfold nextblock; simpl. Simpl. erewrite exec_straight_pc; eauto.
 Qed.
 
+
+
 (** The following lemmas show that straight-line executions
   (predicate [exec_straight_blocks]) correspond to correct Asm executions. *)