Merge remote-tracking branch 'origin/mppa-work' into mppa-peephole

10 files changed, 61 insertions, 93 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 1988813f..9abc1ca1 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -264,13 +264,13 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := parexec
 
 (** 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) := parexec_load_offset chunk rs rs m m d a ofs.
 
 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_load_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_regxs 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_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := parexec_store_offset 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.
 
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 04f02a80..2b6a8450 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -135,7 +135,7 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
 
 Definition exec_load_deps_offset (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) :=
   let (ge, fn) := Ge in
-  match (eval_offset ge ofs) with
+  match (eval_offset ofs) with
   | OK ptr => match Mem.loadv chunk m (Val.offset_ptr v ptr) with 
               | None => None
               | Some vl => Some (Val vl)
@@ -165,7 +165,7 @@ Definition load_eval (lo: load_op) (l: list value) :=
 
 Definition exec_store_deps_offset (chunk: memory_chunk) (m: mem) (vs va: val) (ofs: offset) :=
   let (ge, fn) := Ge in
-  match (eval_offset ge ofs) with
+  match (eval_offset ofs) with
   | OK ptr => match Mem.storev chunk m (Val.offset_ptr va ptr) vs with
               | None => None
               | Some m' => Some (Memstate m')
@@ -845,7 +845,8 @@ Proof.
     (* Load Offset *)
     + destruct i; simpl load_chunk. all:
       unfold parexec_load_offset; simpl; unfold exec_load_deps_offset; erewrite GENV, H, H0;
-      destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto;
+      unfold eval_offset;
+      simpl; auto;
       destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto;
       eexists; split; try split; Simpl;
       intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
@@ -869,7 +870,7 @@ Proof.
     (* Store Offset *)
     + destruct i; simpl store_chunk. all:
       unfold parexec_store_offset; simpl; unfold exec_store_deps_offset; erewrite GENV, H, H0; rewrite (H0 ra);
-      destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto;
+      unfold eval_offset; simpl; auto;
       destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto;
       eexists; split; try split; Simpl;
       intros rr; destruct rr; Simpl.
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index ca7094da..dc55715a 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -803,7 +803,7 @@ Definition indexed_memory_access
         (base: ireg) (ofs: ptrofs) :=
   match make_immed64 (Ptrofs.to_int64 ofs) with
   | Imm64_single imm =>
-      mk_instr base (Ofsimm (Ptrofs.of_int64 imm))
+      mk_instr base (Ptrofs.of_int64 imm)
 end.
 
 Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) :=
@@ -868,7 +868,7 @@ Definition transl_memory_access
       do rs <- ireg_of a1;
       OK (indexed_memory_access mk_instr rs ofs ::i k)
   | Aglobal id ofs, nil =>
-      OK (Ploadsymbol id ofs RTMP ::i (mk_instr RTMP (Ofsimm Ptrofs.zero) ::i k))
+      OK (Ploadsymbol id ofs RTMP ::i (mk_instr RTMP Ptrofs.zero ::i k))
   | Ainstack ofs, nil =>
       OK (indexed_memory_access mk_instr SP ofs ::i k)
   | _, _ =>
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index b265f221..c3ee28f1 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1872,7 +1872,7 @@ Lemma indexed_memory_access_correct:
   exists base' ofs' rs' ptr',
      exec_straight_opt (indexed_memory_access mk_instr base ofs ::g k) rs m
                        (mk_instr base' ofs' ::g k) rs' m
-  /\ eval_offset ge ofs' = OK ptr'
+  /\ eval_offset ofs' = OK ptr'
   /\ Val.offset_ptr rs'#base' ptr' = Val.offset_ptr rs#base ofs
   /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
 Proof.
@@ -1917,7 +1917,7 @@ Qed.
 Lemma indexed_load_access_correct:
   forall chunk (mk_instr: ireg -> offset -> basic) rd m,
   (forall base ofs rs,
-     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs) ->
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs) ->
   forall (base: ireg) ofs k (rs: regset) v,
   Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v ->
   base <> RTMP ->
@@ -1938,7 +1938,7 @@ Qed.
 Lemma indexed_store_access_correct:
   forall chunk (mk_instr: ireg -> offset -> basic) r1 m,
   (forall base ofs rs,
-     exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk rs m r1 base ofs) ->
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk rs m r1 base ofs) ->
   forall (base: ireg) ofs k (rs: regset) m',
   Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' ->
   base <> RTMP -> r1 <> RTMP ->
@@ -1974,7 +1974,7 @@ Proof.
              /\ c = indexed_memory_access mk_instr base ofs :: k
              /\ forall base' ofs' rs',
                    exec_basic_instr ge (mk_instr base' ofs') rs' m =
-                   exec_load_offset ge (chunk_of_type ty) rs' m rd base' ofs').
+                   exec_load_offset (chunk_of_type ty) rs' m rd base' ofs').
   { unfold loadind in TR.
     destruct ty, (preg_of dst); inv TR; econstructor; esplit; eauto. }
   destruct A as (mk_instr & rd & rdEq & B & C). subst c. rewrite rdEq.
@@ -1996,7 +1996,7 @@ Proof.
              /\ c = indexed_memory_access mk_instr base ofs :: k
              /\ forall base' ofs' rs',
                    exec_basic_instr ge (mk_instr base' ofs') rs' m =
-                   exec_store_offset ge (chunk_of_type ty) rs' m rr base' ofs').
+                   exec_store_offset (chunk_of_type ty) rs' m rr base' ofs').
   { unfold storeind in TR. destruct ty, (preg_of src); inv TR; econstructor; esplit; eauto. }
   destruct A as (mk_instr & rr & rsEq & B & C). subst c.
   eapply indexed_store_access_correct; eauto with asmgen.
@@ -2066,7 +2066,7 @@ Lemma transl_memory_access_correct:
   eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
   exists base ofs rs' ptr,
      exec_straight_opt (basics_to_code c) rs m (mk_instr base ofs ::g (basics_to_code k)) rs' m
-  /\ eval_offset ge ofs = OK ptr
+  /\ eval_offset ofs = OK ptr
   /\ Val.offset_ptr rs'#base ptr = v
   /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
 Proof.
@@ -2183,7 +2183,7 @@ Qed.
 Lemma transl_load_access_correct:
   forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v',
   (forall base ofs rs,
-     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs) ->
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs) ->
   transl_memory_access mk_instr addr args k = OK c ->
   eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
   Mem.loadv chunk m v = Some v' ->
@@ -2211,7 +2211,7 @@ Lemma transl_load_memory_access_ok:
      preg_of dst = IR rd
   /\ transl_memory_access mk_instr addr args k = OK c
   /\ forall base ofs rs,
-        exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs.
+        exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset chunk rs m rd base ofs.
 Proof.
   intros until m. intros ADDR TR ? ?.
   unfold transl_load in TR. destruct addr; try contradiction.
@@ -2347,7 +2347,7 @@ Qed.
 Lemma transl_store_access_correct:
   forall chunk (mk_instr: ireg -> offset -> basic) addr args k c r1 (rs: regset) m v m',
   (forall base ofs rs,
-     exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk rs m r1 base ofs) ->
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk rs m r1 base ofs) ->
   transl_memory_access mk_instr addr args k = OK c ->
   eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
   Mem.storev chunk m v rs#r1 = Some m' ->
@@ -2368,16 +2368,16 @@ 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.
+  exec_store_offset Mint8unsigned rs m x base ofs = exec_store_offset Mint8signed rs m x base ofs.
 Proof.
-  unfold exec_store_offset. unfold parexec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev.
+  unfold exec_store_offset. unfold parexec_store_offset. unfold 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.
+  exec_store_offset Mint16unsigned rs m x base ofs = exec_store_offset Mint16signed rs m x base ofs.
 Proof.
-  unfold exec_store_offset. unfold parexec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev.
+  unfold exec_store_offset. unfold parexec_store_offset. unfold eval_offset; auto. unfold Mem.storev.
   destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_16. reflexivity.
 Qed.
 
@@ -2391,7 +2391,7 @@ Lemma transl_store_memory_access_ok:
      preg_of src = IR rr
   /\ transl_memory_access mk_instr addr args k = OK c
   /\ (forall base ofs rs,
-       exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk' rs m rr base ofs)
+       exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset chunk' rs m rr base ofs)
   /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src).
 Proof.
   intros until m'. intros ? TR ? ?.
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index ba771bcb..c49cfbd5 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -154,10 +154,10 @@ let expand_builtin_memcpy_big sz al src dst =
   let lbl = new_label() in
   emit (Ploopdo (tmpbuf, lbl));
   emit Psemi;
-  emit (Plb (tmpbuf, srcptr, AOff (Asmvliw.Ofsimm Z.zero)));
+  emit (Plb (tmpbuf, srcptr, AOff Z.zero));
   emit (Paddil (srcptr, srcptr, Z.one));
   emit Psemi;
-  emit (Psb (tmpbuf, dstptr, AOff (Asmvliw.Ofsimm Z.zero)));
+  emit (Psb (tmpbuf, dstptr, AOff Z.zero));
   emit (Paddil (dstptr, dstptr, Z.one));
   emit Psemi;
   emit (Plabel lbl);;
@@ -173,30 +173,30 @@ let expand_builtin_memcpy  sz al args =
 let expand_builtin_vload_common chunk base ofs res =
   match chunk, res with
   | Mint8unsigned, BR(Asmvliw.IR res) ->
-     emit (Plbu (res, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Plbu (res, base, AOff ofs))
   | Mint8signed, BR(Asmvliw.IR res) ->
-     emit (Plb  (res, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Plb  (res, base, AOff ofs))
   | Mint16unsigned, BR(Asmvliw.IR res) ->
-     emit (Plhu (res, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Plhu (res, base, AOff ofs))
   | Mint16signed, BR(Asmvliw.IR res) ->
-     emit (Plh  (res, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Plh  (res, base, AOff ofs))
   | Mint32, BR(Asmvliw.IR res) ->
-     emit (Plw  (res, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Plw  (res, base, AOff ofs))
   | Mint64, BR(Asmvliw.IR res) ->
-     emit (Pld  (res, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Pld  (res, base, AOff ofs))
   | Mint64, BR_splitlong(BR(Asmvliw.IR res1), BR(Asmvliw.IR res2)) ->
      let ofs' = Ptrofs.add ofs _4 in
      if base <> res2 then begin
-         emit (Plw (res2, base, AOff (Asmvliw.Ofsimm ofs)));
-         emit (Plw (res1, base, AOff (Asmvliw.Ofsimm ofs')))
+         emit (Plw (res2, base, AOff ofs));
+         emit (Plw (res1, base, AOff ofs'))
        end else begin
-         emit (Plw (res1, base, AOff (Asmvliw.Ofsimm ofs')));
-         emit (Plw (res2, base, AOff (Asmvliw.Ofsimm ofs)))
+         emit (Plw (res1, base, AOff ofs'));
+         emit (Plw (res2, base, AOff ofs))
        end
   | Mfloat32, BR(Asmvliw.IR res) ->
-     emit (Pfls (res, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Pfls (res, base, AOff ofs))
   | Mfloat64, BR(Asmvliw.IR res) ->
-     emit (Pfld (res, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Pfld (res, base, AOff ofs))
   | _ ->
      assert false
 
@@ -215,21 +215,21 @@ let expand_builtin_vload chunk args res =
 let expand_builtin_vstore_common chunk base ofs src =
   match chunk, src with
   | (Mint8signed | Mint8unsigned), BA(Asmvliw.IR src) ->
-     emit (Psb (src, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Psb (src, base, AOff ofs))
   | (Mint16signed | Mint16unsigned), BA(Asmvliw.IR src) ->
-     emit (Psh (src, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Psh (src, base, AOff ofs))
   | Mint32, BA(Asmvliw.IR src) ->
-     emit (Psw (src, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Psw (src, base, AOff ofs))
   | Mint64, BA(Asmvliw.IR src) ->
-     emit (Psd (src, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Psd (src, base, AOff ofs))
   | Mint64, BA_splitlong(BA(Asmvliw.IR src1), BA(Asmvliw.IR src2)) ->
      let ofs' = Ptrofs.add ofs _4 in
-     emit (Psw (src2, base, AOff (Asmvliw.Ofsimm ofs)));
-     emit (Psw (src1, base, AOff (Asmvliw.Ofsimm ofs')))
+     emit (Psw (src2, base, AOff ofs));
+     emit (Psw (src1, base, AOff ofs'))
   | Mfloat32, BA(Asmvliw.IR src) ->
-     emit (Pfss (src, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Pfss (src, base, AOff ofs))
   | Mfloat64, BA(Asmvliw.IR src) ->
-     emit (Pfsd (src, base, AOff (Asmvliw.Ofsimm ofs)))
+     emit (Pfsd (src, base, AOff ofs))
   | _ ->
      assert false
 
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index fb1575f9..248b8660 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -203,9 +203,7 @@ Inductive ftest: Type :=
 (** Offsets for load and store instructions.  An offset is either an
   immediate integer or the low part of a symbol. *)
 
-Inductive offset : Type :=
-  | Ofsimm (ofs: ptrofs)
-  | Ofslow (id: ident) (ofs: ptrofs).
+Definition offset : Type := ptrofs.
 
 (** We model a subset of the K1c instruction set. In particular, we do not
   support floats yet.
@@ -1141,15 +1139,7 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset :=
   | PArithARRI64 n d s i => rsw#d <- (arith_eval_arri64 n rsr#d rsr#s i)
   end.
 
-Definition eval_offset (ofs: offset) : res ptrofs :=
-  match ofs with
-  | Ofsimm n => OK n
-  | Ofslow id delta => 
-      match (Genv.symbol_address ge id delta) with
-      | Vptr b ofs => OK ofs
-      | _ => Error (msg "Asmblock.eval_offset")
-      end
-  end.
+Definition eval_offset (ofs: offset) : res ptrofs := OK ofs.
 
 (** * load/store *)
 
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index abc3dcb6..033cf943 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -544,9 +544,8 @@ exception InvalidEncoding
 
 let rec_to_usage r =
   let encoding = match r.imm with None -> None | Some (I32 i) | Some (I64 i) -> Some (encode_imm @@ Z.to_int64 i)
-                                  | Some (Off (Ofsimm ptr)) -> Some (encode_imm @@ camlint64_of_ptrofs ptr)
-                                  | Some (Off (Ofslow (_, _))) -> Some E27U27L10 (* FIXME *) 
-                                  (* I do not know yet in which context Ofslow can be used by CompCert *)
+                                  | Some (Off ptr) -> Some (encode_imm @@ camlint64_of_ptrofs ptr)
+
   and real_inst = ab_inst_to_real r.inst
   in match real_inst with
   | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 43c8acb8..47248e3e 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -96,11 +96,11 @@ Proof.
 Qed.
 
 Lemma exec_load_offset_pc_var:
-  forall ge t rs m rd ra ofs rs' m' v,
-  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'.
+  forall t rs m rd ra ofs rs' m' v,
+  exec_load_offset t rs m rd ra ofs = Next rs' m' ->
+  exec_load_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_load_offset in *. unfold parexec_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 ofs); try discriminate.
   destruct (Mem.loadv _ _ _).
   - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
   - discriminate.
@@ -129,12 +129,12 @@ Proof.
 Qed.
 
 Lemma exec_store_offset_pc_var:
-  forall ge t rs m rd ra ofs rs' m' v,
-  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'.
+  forall t rs m rd ra ofs rs' m' v,
+  exec_store_offset t rs m rd ra ofs = Next rs' m' ->
+  exec_store_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
 Proof.
   intros. unfold exec_store_offset in *. unfold parexec_store_offset in *. rewrite Pregmap.gso; try discriminate.
-  destruct (eval_offset ge ofs); try discriminate.
+  destruct (eval_offset ofs); try discriminate.
   destruct (Mem.storev _ _ _).
   - inv H. apply next_eq; auto.
   - discriminate.
@@ -600,32 +600,12 @@ Proof.
     unfold par_goto_label; unfold par_eval_branch; unfold par_goto_label; erewrite label_pos_preserved_blocks; eauto.
 Qed.
 
-Lemma eval_offset_preserved:
-  forall ofs, eval_offset ge ofs = eval_offset tge ofs.
-Proof.
-  intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto.
-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. 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. 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. 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.
+  unfold parexec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence.
 Qed.
 
 Lemma transf_exec_body:
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 62b02f58..156b16d0 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -160,9 +160,7 @@ module Target (*: TARGET*) =
   *)
 (* Offset part of a load or store *)
 
-    let offset oc = let open Asmvliw in function
-    | Ofsimm n -> ptrofs oc n
-    | Ofslow(id, ofs) -> fprintf oc "%%lo(%a)" symbol_offset (id, ofs)
+    let offset oc n = ptrofs oc n 
 
     let addressing oc = function
     | AOff ofs -> offset oc ofs
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index a93cb28a..0465618c 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -944,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 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_offset in H1; destruct (eval_offset 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_load_regxs 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_offset in H1; destruct (eval_offset 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.
   1-10: try (unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
   - (* PStoreQRRO *)