We now generate load/store with 3 registers (ld rd rs1[rs2]), proofs admitted

3 files changed, 51 insertions, 494 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index f207b64d..54a1b0f4 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -741,11 +741,7 @@ Definition indexed_memory_access
   match make_immed64 (Ptrofs.to_int64 ofs) with
   | Imm64_single imm =>
       mk_instr base (Ofsimm (Ptrofs.of_int64 imm))
-(*| Imm64_pair hi lo =>
-      Pluil GPR31 hi :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm (Ptrofs.of_int64 lo)) :: k
-  | Imm64_large imm =>
-      Pmake GPR31 imm :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm Ptrofs.zero) :: k
-*)end.
+end.
 
 Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) :=
   match ty, preg_of dst with
@@ -777,6 +773,17 @@ Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) :=
 
 (** Translation of memory accesses: loads, and stores. *)
 
+Definition transl_memory_access2
+     (mk_instr: ireg -> ireg -> basic)
+     (addr: addressing) (args: list mreg) (k: bcode) : res bcode :=
+  match addr, args with
+  | Aindexed2, a1 :: a2 :: nil =>
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (mk_instr rs1 rs2 ::i k)
+  | _, _ => Error (msg "Asmblockgen.transl_memory_access2")
+  end.
+
 Definition transl_memory_access
      (mk_instr: ireg -> offset -> basic)
      (addr: addressing) (args: list mreg) (k: bcode) : res bcode :=
@@ -806,10 +813,22 @@ Definition chunk2load (chunk: memory_chunk) :=
   | Many64 => Pld_a
   end.
 
-Definition transl_load (chunk: memory_chunk) (addr: addressing)
+Definition transl_load_rro (chunk: memory_chunk) (addr: addressing)
            (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
   do r <- ireg_of dst;
-  transl_memory_access (chunk2load chunk r) addr args k.
+  transl_memory_access (PLoadRRO (chunk2load chunk) r) addr args k.
+
+Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing)
+           (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
+  do r <- ireg_of dst;
+  transl_memory_access2 (PLoadRRR (chunk2load chunk) r) addr args k.
+
+Definition transl_load (chunk: memory_chunk) (addr: addressing)
+           (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
+  match args with
+  | a1 :: a2 :: nil => transl_load_rrr chunk addr args dst k
+  | _ => transl_load_rro chunk addr args dst k
+  end.
 
 Definition chunk2store (chunk: memory_chunk) :=
   match chunk with
@@ -823,10 +842,22 @@ Definition chunk2store (chunk: memory_chunk) :=
   | Many64 => Psd_a
   end.
 
-Definition transl_store (chunk: memory_chunk) (addr: addressing)
+Definition transl_store_rro (chunk: memory_chunk) (addr: addressing)
+           (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
+  do r <- ireg_of src;
+  transl_memory_access (PStoreRRO (chunk2store chunk) r) addr args k.
+
+Definition transl_store_rrr (chunk: memory_chunk) (addr: addressing)
            (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
   do r <- ireg_of src;
-  transl_memory_access (chunk2store chunk r) addr args k.
+  transl_memory_access2 (PStoreRRR (chunk2store chunk) r) addr args k.
+
+Definition transl_store (chunk: memory_chunk) (addr: addressing)
+           (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
+  match args with
+  | a1 :: a2 :: nil => transl_store_rrr chunk addr args src k
+  | _ => transl_load_rro chunk addr args src k
+  end.
 
 (** Function epilogue *)
 
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 63f4c136..81474d30 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -16,7 +16,6 @@ Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.

 Require Import Values Memory Events Globalenvs Smallstep.

 Require Import Op Locations Machblock Conventions Asmblock.

-(* Require Import Asmgen Asmgenproof0 Asmgenproof1. *)

 Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1.

 

 Module MB := Machblock.

@@ -75,34 +74,6 @@ Proof.
   omega.

 Qed.

 

-(*

-Lemma exec_straight_exec:

-  forall fb f c ep tf tc c' rs m rs' m',

-  transl_code_at_pc ge (rs PC) fb f c ep tf tc ->

-  exec_straight tge tf tc rs m c' rs' m' ->

-  plus step tge (State rs m) E0 (State rs' m').

-Proof.

-  intros. inv H.

-  eapply exec_straight_steps_1; eauto.

-  eapply transf_function_no_overflow; eauto.

-  eapply functions_transl; eauto.

-Qed.

-

-Lemma exec_straight_at:

-  forall fb f c ep tf tc c' ep' tc' rs m rs' m',

-  transl_code_at_pc ge (rs PC) fb f c ep tf tc ->

-  transl_code f c' ep' = OK tc' ->

-  exec_straight tge tf tc rs m tc' rs' m' ->

-  transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'.

-Proof.

-  intros. inv H.

-  exploit exec_straight_steps_2; eauto.

-  eapply transf_function_no_overflow; eauto.

-  eapply functions_transl; eauto.

-  intros [ofs' [PC' CT']].

-  rewrite PC'. constructor; auto.

-Qed.

- *)

 (** The following lemmas show that the translation from Mach to Asm

   preserves labels, in the sense that the following diagram commutes:

 <<

@@ -121,314 +92,6 @@ Qed.
 

 Section TRANSL_LABEL.

 

-(* Remark loadimm32_label:

-  forall r n k, tail_nolabel k (loadimm32 r n k).

-Proof.

-  intros; unfold loadimm32. destruct (make_immed32 n); TailNoLabel.

-(*unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.*)

-Qed.

-Hint Resolve loadimm32_label: labels.

-

-Remark opimm32_label:

-  forall (op: arith_name_rrr) (opimm: arith_name_rri32) r1 r2 n k,

-  (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->

-  (forall r1 r2 n, nolabel (opimm r1 r2 n)) ->

-  tail_nolabel k (opimm32 op opimm r1 r2 n k).

-Proof.

-  intros; unfold opimm32. destruct (make_immed32 n); TailNoLabel.

-(*unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.*)

-Qed.

-Hint Resolve opimm32_label: labels.

-

-Remark loadimm64_label:

-  forall r n k, tail_nolabel k (loadimm64 r n k).

-Proof.

-  intros; unfold loadimm64. destruct (make_immed64 n); TailNoLabel.

-(*unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.*)

-Qed.

-Hint Resolve loadimm64_label: labels.

-

-Remark cast32signed_label:

-  forall rd rs k, tail_nolabel k (cast32signed rd rs k).

-Proof.

-  intros; unfold cast32signed. destruct (ireg_eq rd rs); TailNoLabel.

-Qed.

-Hint Resolve cast32signed_label: labels.

-

-Remark opimm64_label:

-  forall (op: arith_name_rrr) (opimm: arith_name_rri64) r1 r2 n k,

-  (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->

-  (forall r1 r2 n, nolabel (opimm r1 r2 n)) ->

-  tail_nolabel k (opimm64 op opimm r1 r2 n k).

-Proof.

-  intros; unfold opimm64. destruct (make_immed64 n); TailNoLabel.

-(*unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.*)

-Qed.

-Hint Resolve opimm64_label: labels.

-

-Remark addptrofs_label:

-  forall r1 r2 n k, tail_nolabel k (addptrofs r1 r2 n k).

-Proof.

-  unfold addptrofs; intros. destruct (Ptrofs.eq_dec n Ptrofs.zero). TailNoLabel.

-  apply opimm64_label; TailNoLabel.

-Qed.

-Hint Resolve addptrofs_label: labels.

-(*

-Remark transl_cond_float_nolabel:

-  forall c r1 r2 r3 insn normal,

-  transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn.

-Proof.

-  unfold transl_cond_float; intros. destruct c; inv H; exact I.

-Qed.

-

-Remark transl_cond_single_nolabel:

-  forall c r1 r2 r3 insn normal,

-  transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn.

-Proof.

-  unfold transl_cond_single; intros. destruct c; inv H; exact I.

-Qed.

-*)

-Remark transl_cbranch_label:

-  forall cond args lbl k c,

-  transl_cbranch cond args lbl k = OK c -> tail_nolabel k c.

-Proof.

-  intros. unfold transl_cbranch in H. destruct cond; TailNoLabel.

-(* Ccomp *)

-  - unfold transl_comp; TailNoLabel.

-(* Ccompu *)

-  - unfold transl_comp; TailNoLabel.

-(* Ccompimm *)

-  - destruct (Int.eq n Int.zero); TailNoLabel.

-    unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.

-(* Ccompuimm *)

-  - unfold transl_opt_compuimm.

-    remember (select_comp n c0) as selcomp; destruct selcomp.

-    + destruct c; TailNoLabel; contradict Heqselcomp; unfold select_comp;

-      destruct (Int.eq n Int.zero); destruct c0; discriminate.

-    + unfold loadimm32;

-      destruct (make_immed32 n); TailNoLabel; unfold transl_comp; TailNoLabel.

-(* Ccompl *)

-  - unfold transl_compl; TailNoLabel.

-(* Ccomplu *)

-  - unfold transl_compl; TailNoLabel.

-(* Ccomplimm *)

-  - destruct (Int64.eq n Int64.zero); TailNoLabel.

-    unfold loadimm64. destruct (make_immed64 n); TailNoLabel. unfold transl_compl; TailNoLabel.

-(* Ccompluimm *)

-  - unfold transl_opt_compluimm.

-    remember (select_compl n c0) as selcomp; destruct selcomp.

-    + destruct c; TailNoLabel; contradict Heqselcomp; unfold select_compl;

-      destruct (Int64.eq n Int64.zero); destruct c0; discriminate.

-    + unfold loadimm64;

-      destruct (make_immed64 n); TailNoLabel; unfold transl_compl; TailNoLabel.

-Qed.

-

-(*

-- destruct c0; simpl; TailNoLabel.

-- destruct c0; simpl; TailNoLabel.

-- destruct (Int.eq n Int.zero).

-  destruct c0; simpl; TailNoLabel.

-  apply tail_nolabel_trans with (transl_cbranch_int32s c0 x X31 lbl :: k).

-  auto with labels. destruct c0; simpl; TailNoLabel.

-- destruct (Int.eq n Int.zero).

-  destruct c0; simpl; TailNoLabel.

-  apply tail_nolabel_trans with (transl_cbranch_int32u c0 x X31 lbl :: k).

-  auto with labels. destruct c0; simpl; TailNoLabel.

-- destruct c0; simpl; TailNoLabel.

-- destruct c0; simpl; TailNoLabel.

-- destruct (Int64.eq n Int64.zero).

-  destruct c0; simpl; TailNoLabel.

-  apply tail_nolabel_trans with (transl_cbranch_int64s c0 x X31 lbl :: k).

-  auto with labels. destruct c0; simpl; TailNoLabel.

-- destruct (Int64.eq n Int64.zero).

-  destruct c0; simpl; TailNoLabel.

-  apply tail_nolabel_trans with (transl_cbranch_int64u c0 x X31 lbl :: k).

-  auto with labels. destruct c0; simpl; TailNoLabel.

-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.

-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 

-  destruct normal; TailNoLabel.

-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.

-  apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. 

-  destruct normal; TailNoLabel.

-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.

-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 

-  destruct normal; TailNoLabel.

-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.

-  apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. 

-  destruct normal; TailNoLabel.

-*)

-

-Remark transl_cond_op_label:

-  forall cond args r k c,

-  transl_cond_op cond r args k = OK c -> tail_nolabel k c.

-Proof.

-  intros. unfold transl_cond_op in H; destruct cond; TailNoLabel.

-- unfold transl_cond_int32s; destruct c0; simpl; TailNoLabel.

-- unfold transl_cond_int32u; destruct c0; simpl; TailNoLabel. 

-- unfold transl_condimm_int32s; destruct c0; simpl; TailNoLabel.

-- unfold transl_condimm_int32u; destruct c0; simpl; TailNoLabel.

-- unfold transl_cond_int64s; destruct c0; simpl; TailNoLabel.

-- unfold transl_cond_int64u; destruct c0; simpl; TailNoLabel. 

-- unfold transl_condimm_int64s; destruct c0; simpl; TailNoLabel.

-- unfold transl_condimm_int64u; destruct c0; simpl; TailNoLabel.

-Qed.

-

-Remark transl_op_label:

-  forall op args r k c,

-  transl_op op args r k = OK c -> tail_nolabel k c.

-Proof.

-Opaque Int.eq.

-  unfold transl_op; intros; destruct op; TailNoLabel.

-(* Omove *)

-- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.

-(* Oaddrsymbol *)

-- destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)); TailNoLabel.

-(* Oaddimm32 *)

-- apply opimm32_label; intros; exact I.

-(* Oandimm32 *)

-- apply opimm32_label; intros; exact I.

-(* Oorimm32 *)

-- apply opimm32_label; intros; exact I.

-(* Oxorimm32 *)

-- apply opimm32_label; intros; exact I.

-(* Oshrximm *)

-- destruct (Int.eq n Int.zero); TailNoLabel.

-(* Oaddimm64 *)

-- apply opimm64_label; intros; exact I.

-(* Oandimm64  *)

-- apply opimm64_label; intros; exact I.

-(* Oorimm64  *)

-- apply opimm64_label; intros; exact I.

-(* Oxorimm64  *)

-- apply opimm64_label; intros; exact I.

-(* Ocmp *)

-- eapply transl_cond_op_label; eauto.

-Qed.

-

-(*

-- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.

-- destruct (Float.eq_dec n Float.zero); TailNoLabel.

-- destruct (Float32.eq_dec n Float32.zero); TailNoLabel.

-- destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).

-+ eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel.

-+ TailNoLabel. 

-- apply opimm32_label; intros; exact I.

-- apply opimm32_label; intros; exact I.

-- apply opimm32_label; intros; exact I.

-- apply opimm32_label; intros; exact I.

-- destruct (Int.eq n Int.zero); TailNoLabel.

-- apply opimm64_label; intros; exact I.

-- apply opimm64_label; intros; exact I.

-- apply opimm64_label; intros; exact I.

-- apply opimm64_label; intros; exact I.

-- destruct (Int.eq n Int.zero); TailNoLabel.

-- eapply transl_cond_op_label; eauto.

-*)

-*)

-

-(* Remark indexed_memory_access_label:

-  forall (mk_instr: ireg -> offset -> instruction) base ofs k,

-  (forall r o, nolabel (mk_instr r o)) ->

-  tail_nolabel k (indexed_memory_access mk_instr base ofs k).

-Proof.

-  unfold indexed_memory_access; intros. 

-  (* destruct Archi.ptr64. *)

-  destruct (make_immed64 (Ptrofs.to_int64 ofs)); TailNoLabel.

-  (* destruct (make_immed32 (Ptrofs.to_int ofs)); TailNoLabel. *)

-Qed. *)

-

-(*

-Remark loadind_label:

-  forall base ofs ty dst k c,

-  loadind base ofs ty dst k = OK c -> tail_nolabel k c.

-Proof.

-  unfold loadind; intros.

-  destruct ty, (preg_of dst); inv H; apply indexed_memory_access_label; intros; exact I.

-Qed.

-

-Remark storeind_label:

-  forall src base ofs ty k c,

-  storeind src base ofs ty k = OK c -> tail_nolabel k c.

-Proof.

-  unfold storeind; intros.

-  destruct ty, (preg_of src); inv H; apply indexed_memory_access_label; intros; exact I.

-Qed.

-

-Remark loadind_ptr_label:

-  forall base ofs dst k, tail_nolabel k (loadind_ptr base ofs dst k).

-Proof.

-  intros. apply indexed_memory_access_label. intros; destruct Archi.ptr64; exact I.

-Qed.

-*)

-

-(* Remark storeind_ptr_label:

-  forall src base ofs k, tail_nolabel k (storeind_ptr src base ofs k).

-Proof.

-  intros. apply indexed_memory_access_label. intros; destruct Archi.ptr64; exact I.

-Qed. *)

-

-(*

-Remark transl_memory_access_label:

-  forall (mk_instr: ireg -> offset -> instruction) addr args k c,

-  (forall r o, nolabel (mk_instr r o)) ->

-  transl_memory_access mk_instr addr args k = OK c ->

-  tail_nolabel k c.

-Proof.

-  unfold transl_memory_access; intros; destruct addr; TailNoLabel; apply indexed_memory_access_label; auto. 

-Qed.

-

-Remark make_epilogue_label:

-  forall f k, tail_nolabel k (make_epilogue f k).

-Proof.

-  unfold make_epilogue; intros. eapply tail_nolabel_trans. apply loadind_ptr_label. TailNoLabel.

-Qed.

-

-Lemma transl_instr_label:

-  forall f i ep k c,

-  transl_instr f i ep k = OK c ->

-  match i with Mlabel lbl => c = Plabel lbl ::i k | _ => tail_nolabel k c end.

-Proof.

-  unfold transl_instr; intros; destruct i; TailNoLabel.

-(* loadind *)

-- eapply loadind_label; eauto.

-(* storeind *)

-- eapply storeind_label; eauto.

-(* Mgetparam *)

-- destruct ep. eapply loadind_label; eauto.

-  eapply tail_nolabel_trans. apply loadind_ptr_label. eapply loadind_label; eauto. 

-(* transl_op *)

-- eapply transl_op_label; eauto.

-(* transl_load *)

-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.

-(* transl store *)

-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.

-- destruct s0; monadInv H; TailNoLabel.

-- destruct s0; monadInv H; eapply tail_nolabel_trans

-  ; [eapply make_epilogue_label|TailNoLabel].

-- eapply transl_cbranch_label; eauto.

-- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].

-Qed.

-(*

-

-

-- eapply transl_op_label; eauto.

-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.

-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.

-- destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]).

-- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].

-*)

-

-Lemma transl_instr_label':

-  forall lbl f i ep k c,

-  transl_instr f i ep k = OK c ->

-  find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k.

-Proof.

-  intros. exploit transl_instr_label; eauto.

-  destruct i; try (intros [A B]; apply B).

-  intros. subst c. simpl. auto.

-Qed.

-*)

-

 Lemma gen_bblocks_label:

   forall hd bdy ex tbb tc,

   gen_bblocks hd bdy ex = tbb::tc ->

@@ -640,115 +303,6 @@ Qed.
 - Mach register values and Asm register values agree.

 *)

 

-(*

-Lemma exec_straight_steps:

-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2,

-  match_stack ge s ->

-  Mem.extends m2 m2' ->

-  Genv.find_funct_ptr ge fb = Some (Internal f) ->

-  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->

-  (forall k c (TR: transl_instr f i ep k = OK c),

-   exists rs2,

-       exec_straight tge tf c rs1 m1' k rs2 m2'

-    /\ agree ms2 sp rs2

-    /\ (fp_is_parent ep i = true -> rs2#FP = parent_sp s)) ->

-  exists st',

-  plus step tge (State rs1 m1') E0 st' /\

-  match_states (Mach.State s fb sp c ms2 m2) st'.

-Proof.

-  intros. inversion H2. subst. monadInv H7.

-  exploit H3; eauto. intros [rs2 [A [B C]]].

-  exists (State rs2 m2'); split.

-  eapply exec_straight_exec; eauto.

-  econstructor; eauto. eapply exec_straight_at; eauto.

-Qed.

-*)

-

-(*

-Lemma exec_straight_steps_goto:

-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',

-  match_stack ge s ->

-  Mem.extends m2 m2' ->

-  Genv.find_funct_ptr ge fb = Some (Internal f) ->

-  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->

-  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->

-  fp_is_parent ep i = false ->

-  (forall k c (TR: transl_instr f i ep k = OK c),

-   exists jmp, exists k', exists rs2,

-       exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2'

-    /\ agree ms2 sp rs2

-    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') ->

-  exists st',

-  plus step tge (State rs1 m1') E0 st' /\

-  match_states (Mach.State s fb sp c' ms2 m2) st'.

-Proof.

-  intros. inversion H3. subst. monadInv H9.

-  exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]].

-  generalize (functions_transl _ _ _ H7 H8); intro FN.

-  generalize (transf_function_no_overflow _ _ H8); intro NOOV.

-  exploit exec_straight_steps_2; eauto.

-  intros [ofs' [PC2 CT2]].

-  exploit find_label_goto_label; eauto.

-  intros [tc' [rs3 [GOTO [AT' OTH]]]].

-  exists (State rs3 m2'); split.

-  eapply plus_right'.

-  eapply exec_straight_steps_1; eauto.

-  econstructor; eauto.

-  eapply find_instr_tail. eauto.

-  rewrite C. eexact GOTO.

-  traceEq.

-  econstructor; eauto.

-  apply agree_exten with rs2; auto with asmgen.

-  congruence.

-Qed.

-

-Lemma exec_straight_opt_steps_goto:

-  forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',

-  match_stack ge s ->

-  Mem.extends m2 m2' ->

-  Genv.find_funct_ptr ge fb = Some (Internal f) ->

-  Mach.find_label lbl f.(Mach.fn_code) = Some c' ->

-  transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->

-  fp_is_parent ep i = false ->

-  (forall k c (TR: transl_instr f i ep k = OK c),

-   exists jmp, exists k', exists rs2,

-       exec_straight_opt tge tf c rs1 m1' (jmp :: k') rs2 m2'

-    /\ agree ms2 sp rs2

-    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') ->

-  exists st',

-  plus step tge (State rs1 m1') E0 st' /\

-  match_states (Mach.State s fb sp c' ms2 m2) st'.

-Proof.

-  intros. inversion H3. subst. monadInv H9.

-  exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]].

-  generalize (functions_transl _ _ _ H7 H8); intro FN.

-  generalize (transf_function_no_overflow _ _ H8); intro NOOV.

-  inv A.

-- exploit find_label_goto_label; eauto.

-  intros [tc' [rs3 [GOTO [AT' OTH]]]].

-  exists (State rs3 m2'); split.

-  apply plus_one. econstructor; eauto.

-  eapply find_instr_tail. eauto.

-  rewrite C. eexact GOTO.

-  econstructor; eauto.

-  apply agree_exten with rs2; auto with asmgen.

-  congruence.

-- exploit exec_straight_steps_2; eauto.

-  intros [ofs' [PC2 CT2]].

-  exploit find_label_goto_label; eauto.

-  intros [tc' [rs3 [GOTO [AT' OTH]]]].

-  exists (State rs3 m2'); split.

-  eapply plus_right'.

-  eapply exec_straight_steps_1; eauto.

-  econstructor; eauto.

-  eapply find_instr_tail. eauto.

-  rewrite C. eexact GOTO.

-  traceEq.

-  econstructor; eauto.

-  apply agree_exten with rs2; auto with asmgen.

-  congruence.

-Qed. *)

-

 (** We need to show that, in the simulation diagram, we cannot

   take infinitely many Mach transitions that correspond to zero

   transitions on the Asm side.  Actually, all Mach transitions

@@ -967,9 +521,9 @@ Proof.
     unfold transl_cond_float32. exploreInst; try discriminate.

     unfold transl_cond_notfloat32. exploreInst; try discriminate.

   - simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate.

-    all: unfold transl_memory_access in EQ0; exploreInst; try discriminate.

+    all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; exploreInst; try discriminate.

   - simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate.

-    all: unfold transl_memory_access in EQ0; exploreInst; try discriminate.

+    all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; exploreInst; try discriminate.

 Qed.

 

 Lemma transl_basic_code_nonil:

@@ -1631,7 +1185,7 @@ Local Transparent destroyed_by_op.
     exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.

     intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.

     exploit Mem.loadv_extends; eauto. intros [v' [C D]].

-    exploit transl_load_correct; eauto.

+    exploit transl_load_correct; eauto. admit.

     intros [rs2 [P [Q R]]].

 

     eapply exec_straight_body in P.

@@ -1658,7 +1212,7 @@ Local Transparent destroyed_by_op.
     intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.

     assert (Val.lessdef (ms src) (rs1 (preg_of src))). eapply preg_val; eauto.

     exploit Mem.storev_extends; eauto. intros [m2' [C D]].

-    exploit transl_store_correct; eauto. intros [rs2 [P Q]].

+    exploit transl_store_correct; eauto. admit. intros [rs2 [P Q]].

 

     eapply exec_straight_body in P.

       2: eapply code_to_basics_id; eauto.

@@ -1673,7 +1227,7 @@ Local Transparent destroyed_by_op.
 

     eapply agree_undef_regs; eauto with asmgen.

     simpl; congruence.

-Qed.

+Admitted.

 

 Lemma exec_body_trans:

   forall l l' rs0 m0 rs1 m1 rs2 m2,

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index f8bbf7f4..06c9fb3e 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -30,40 +30,13 @@ Lemma make_immed32_sound:
 Proof.
   intros; unfold make_immed32. set (lo := Int.sign_ext 12 n).
   predSpec Int.eq Int.eq_spec n lo; auto.
-(*
-- auto.
-- set (m := Int.sub n lo).
-  assert (A: Int.eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto).
-  assert (B: Int.eqmod (two_p 12) (Int.unsigned n - Int.unsigned  lo) 0).
-  { replace 0 with (Int.unsigned n - Int.unsigned n) by omega.
-    auto using Int.eqmod_sub, Int.eqmod_refl. }
-  assert (C: Int.eqmod (two_p 12) (Int.unsigned m) 0).
-  { apply Int.eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto.
-    apply Int.eqmod_divides with Int.modulus. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
-    exists (two_p (32-12)); auto. }
-  assert (D: Int.modu m (Int.repr 4096) = Int.zero).
-  { apply Int.eqmod_mod_eq in C. unfold Int.modu. 
-    change (Int.unsigned (Int.repr 4096)) with (two_p 12). rewrite C. 
-    reflexivity.
-    apply two_p_gt_ZERO; omega. }
-  rewrite <- (Int.divu_pow2 m (Int.repr 4096) (Int.repr 12)) by auto.
-  rewrite Int.shl_mul_two_p. 
-  change (two_p (Int.unsigned (Int.repr 12))) with 4096.
-  replace (Int.mul (Int.divu m (Int.repr 4096)) (Int.repr 4096)) with m.
-  unfold m. rewrite Int.sub_add_opp. rewrite Int.add_assoc. rewrite <- (Int.add_commut lo).
-  rewrite Int.add_neg_zero. rewrite Int.add_zero. auto.
-  rewrite (Int.modu_divu_Euclid m (Int.repr 4096)) at 1 by (vm_compute; congruence).
-  rewrite D. apply Int.add_zero.
-*)
 Qed.
 
 Lemma make_immed64_sound:
   forall n,
   match make_immed64 n with
   | Imm64_single imm => n = imm
-(*| Imm64_pair hi lo => n = Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo
-  | Imm64_large imm => n = imm
-*)end.
+  end.
 Proof.
   intros; unfold make_immed64. set (lo := Int64.sign_ext 12 n).
   predSpec Int64.eq Int64.eq_spec n lo.
@@ -76,7 +49,6 @@ Proof.
 Qed.
 
 
-
 (** Properties of registers *)
 
 Lemma ireg_of_not_RTMP:
@@ -2000,10 +1972,10 @@ Proof.
    /\ 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).
-  { unfold transl_load in TR; destruct chunk; ArgsInv; econstructor; (esplit; eauto). }
+  { (* unfold transl_load in TR; destruct chunk; ArgsInv; econstructor; (esplit; eauto). *) admit. }
   destruct A as (mk_instr & rd & rdEq & B & C). rewrite rdEq.
   eapply transl_load_access_correct; eauto with asmgen.
-Qed.
+Admitted.
 
 Lemma transl_store_correct:
   forall chunk addr args src k c (rs: regset) m a m',
@@ -2021,16 +1993,16 @@ Proof.
    /\ (forall base ofs rs,
         exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk' rs m rr base ofs)
    /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src)).
-  { unfold transl_store in TR; destruct chunk; ArgsInv;
+  { admit. (* unfold transl_store in TR; destruct chunk; ArgsInv;
     (econstructor; econstructor; econstructor; split; [eauto | split; [eassumption | split; [ intros; simpl; reflexivity | auto]]]).
     destruct a; auto. apply Mem.store_signed_unsigned_8. 
-    destruct a; auto. apply Mem.store_signed_unsigned_16. 
+    destruct a; auto. apply Mem.store_signed_unsigned_16.  *)
   }
   destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D).
   rewrite D in STORE; clear D. 
   eapply transl_store_access_correct; eauto with asmgen. congruence.
   destruct rr; try discriminate. destruct src; try discriminate.
-Qed.
+Admitted.
 
 Lemma make_epilogue_correct:
   forall ge0 f m stk soff cs m' ms rs k tm,