MPPA - Started restricting instructions + get/set + change ABI + trying to prove it

3 files changed, 147 insertions, 78 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 21e088fd..f5ff7c78 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -52,6 +52,12 @@ Inductive gpreg: Type :=
 
 Definition ireg := gpreg.
 
+(* FIXME - placeholder definitions to make sure the Risc-V instruction definitions work *)
+Inductive ireg0: Type := 
+  | GPR: gpreg -> ireg0.
+
+Coercion GPR: gpreg >-> ireg0.
+
 Definition freg := gpreg.
 
 Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}.
@@ -85,9 +91,6 @@ Module Pregmap := EMap(PregEq).
 
 Notation "'SP'" := GPR12 (only parsing) : asm.
 
-(* FIXME - placeholder definitions to make sure the Risc-V instruction definitions work *)
-Definition ireg0 := ireg.
-
 (** Offsets for load and store instructions.  An offset is either an
   immediate integer or the low part of a symbol. *)
 
@@ -131,6 +134,10 @@ Definition label := positive.
   [Asmgen]) is careful to respect this range. *)
 
 Inductive instruction : Type :=
+(** Branch Control Unit instructions *)
+  | Pget    (rd: ireg) (rs: preg)                    (**r get system register *)
+  | Pset    (rd: preg) (rs: ireg)                    (**r set system register *)
+  | Pret                                             (**r return *)
 (*
   | Pmv     (rd: ireg) (rs: ireg)                    (**r integer move *)
 
@@ -177,9 +184,9 @@ Inductive instruction : Type :=
   | Psllil  (rd: ireg) (rs: ireg0) (imm: int)        (**r shift-left-logical immediate *)
   | Psrlil  (rd: ireg) (rs: ireg0) (imm: int)        (**r shift-right-logical immediate *)
   | Psrail  (rd: ireg) (rs: ireg0) (imm: int)        (**r shift-right-arith immediate *)
-  | Pluil   (rd: ireg)             (imm: int64)      (**r load upper-immediate *)
+*)| Pluil   (rd: ireg)             (imm: int64)      (**r load upper-immediate *)
 (** 64-bit integer register-register instructions *)
-*)  | Paddl   (rd: ireg) (rs1 rs2: ireg0)              (**r integer addition *) (*
+  | Paddl   (rd: ireg) (rs1 rs2: ireg0)              (**r integer addition *) (*
   | Psubl   (rd: ireg) (rs1 rs2: ireg0)              (**r integer subtraction *)
 
   | Pmull   (rd: ireg) (rs1 rs2: ireg0)              (**r integer multiply low *)
@@ -206,8 +213,8 @@ Inductive instruction : Type :=
   (* Unconditional jumps.  Links are always to X1/RA. *)
   | Pj_l    (l: label)                              (**r jump to label *)
   | Pj_s    (symb: ident) (sg: signature)           (**r jump to symbol *)
-*)| Pj_r    (r: ireg)     (sg: signature)           (**r jump register *)
-(*| Pjal_s  (symb: ident) (sg: signature)           (**r jump-and-link symbol *)
+  | Pj_r    (r: ireg)     (sg: signature)           (**r jump register *)
+  | Pjal_s  (symb: ident) (sg: signature)           (**r jump-and-link symbol *)
   | Pjal_r  (r: ireg)     (sg: signature)           (**r jump-and-link register *)
 
   (* Conditional branches, 32-bit comparisons *)
@@ -233,15 +240,15 @@ Inductive instruction : Type :=
   | Plhu    (rd: ireg) (ra: ireg) (ofs: offset)     (**r load unsigned int16 *)
   | Plw     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int32 *)
   | Plw_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any32 *)
-  | Pld     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int64 *)
-  | Pld_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any64 *)
+*)| Pld     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int64 *)
+(*| Pld_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any64 *)
 
   | Psb     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int8 *)
   | Psh     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int16 *)
   | Psw     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int32 *)
   | Psw_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any32 *)
-  | Psd     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int64 *)
-  | Psd_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any64 *)
+*)| Psd     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int64 *)
+(*| Psd_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any64 *)
 
   (* Synchronization *)
   | Pfence                                          (**r fence *)
@@ -332,8 +339,8 @@ Inductive instruction : Type :=
   | Plabel  (lbl: label)                            (**r define a code label *)
 (*  | Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the address of a symbol *)
   | Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *)
-  | Ploadli (rd: ireg) (i: int64)                   (**r load an immediate int64 *)
-  | Ploadfi (rd: freg) (f: float)                   (**r load an immediate float *)
+*)| Ploadli (rd: ireg) (i: int64)                   (**r load an immediate int64 *)
+(*| Ploadfi (rd: freg) (f: float)                   (**r load an immediate float *)
   | Ploadsi (rd: freg) (f: float32)                 (**r load an immediate single *)
   | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *) *)
   | Pbuiltin: external_function -> list (builtin_arg preg)
@@ -431,19 +438,31 @@ Definition program := AST.program fundef unit.
 Definition regset := Pregmap.t val.
 Definition genv := Genv.t fundef unit.
 
-Definition get0w (rs: regset) (r: ireg0) : val :=
+Definition getw (rs: regset) (r: ireg0) : val :=
+  match r with
+  | GPR r => rs r
+  end.
+(*
   match r with
   | X0 => Vint Int.zero
+  | X r => rs r
   end.
+*)
 
-Definition get0l (rs: regset) (r: ireg0) : val :=
+Definition getl (rs: regset) (r: ireg0) : val :=
+  match r with
+  | GPR r => rs r
+  end.
+(*
   match r with
   | X0 => Vlong Int64.zero
+  | X r => rs r
   end.
+*)
 
 Notation "a # b" := (a b) (at level 1, only parsing) : asm.
-Notation "a ## b" := (get0w a b) (at level 1) : asm.
-Notation "a ### b" := (get0l a b) (at level 1) : asm.
+Notation "a ## b" := (getw a b) (at level 1) : asm.
+Notation "a ### b" := (getl a b) (at level 1) : asm.
 Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
 
 Open Scope asm.
@@ -603,6 +622,18 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti
 
 Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome :=
   match i with
+  | Pget rd ra =>
+    match ra with
+    | RA => Next (nextinstr (rs#rd <- (rs#ra))) m
+    | _  => Stuck
+    end
+  | Pset ra rd =>
+    match ra with
+    | RA => Next (nextinstr (rs#ra <- (rs#rd))) m
+    | _  => Stuck
+    end
+  | Pret =>
+      Next (rs#PC <- (rs#RA)) m
 (*  | Pmv d s =>
       Next (nextinstr (rs#d <- (rs#s))) m
 
@@ -687,11 +718,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (Val.shrlu rs###s (Vint i)))) m
   | Psrail d s i =>
       Next (nextinstr (rs#d <- (Val.shrl rs###s (Vint i)))) m
-  | Pluil d i =>
+*)| Pluil d i =>
       Next (nextinstr (rs#d <- (Vlong (Int64.sign_ext 32 (Int64.shl i (Int64.repr 12)))))) m
 
 (** 64-bit integer register-register instructions *)
-*)| Paddl d s1 s2 =>
+  | Paddl d s1 s2 =>
       Next (nextinstr (rs#d <- (Val.addl rs###s1 rs###s2))) m
 (*| Psubl d s1 s2 =>
       Next (nextinstr (rs#d <- (Val.subl rs###s1 rs###s2))) m
@@ -740,9 +771,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       goto_label f l rs m
   | Pj_s s sg =>
       Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
-*)| Pj_r r sg =>
+  | Pj_r r sg =>
       Next (rs#PC <- (rs#r)) m
-(*| Pjal_s s sg =>
+  | Pjal_s s sg =>
       Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)
               #RA <- (Val.offset_ptr rs#PC Ptrofs.one)
            ) m
@@ -791,9 +822,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       exec_load Mint32 rs m d a ofs
   | Plw_a d a ofs =>
       exec_load Many32 rs m d a ofs
-  | Pld d a ofs =>
+*)| Pld d a ofs =>
       exec_load Mint64 rs m d a ofs
-  | Pld_a d a ofs =>
+(*| Pld_a d a ofs =>
       exec_load Many64 rs m d a ofs
   | Psb s a ofs =>
       exec_store Mint8unsigned rs m s a ofs
@@ -803,9 +834,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       exec_store Mint32 rs m s a ofs
   | Psw_a s a ofs =>
       exec_store Many32 rs m s a ofs
-  | Psd s a ofs =>
+*)| Psd s a ofs =>
       exec_store Mint64 rs m s a ofs
-  | Psd_a s a ofs =>
+(*| Psd_a s a ofs =>
       exec_store Many64 rs m s a ofs
 
 (** Floating point register move *)
@@ -936,9 +967,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#rd <- (Genv.symbol_address ge s ofs))) m
   | Ploadsymbol_high rd s ofs =>
       Next (nextinstr (rs#rd <- (high_half ge s ofs))) m
-  | Ploadli rd i =>
+*)| Ploadli rd i =>
       Next (nextinstr (rs#GPR31 <- Vundef #rd <- (Vlong i))) m
-  | Ploadfi rd f =>
+(*| Ploadfi rd f =>
       Next (nextinstr (rs#GPR31 <- Vundef #rd <- (Vfloat f))) m
   | Ploadsi rd f =>
       Next (nextinstr (rs#GPR31 <- Vundef #rd <- (Vsingle f))) m
@@ -1154,6 +1185,7 @@ Qed.
 Definition data_preg (r: preg) : bool :=
   match r with
   | RA  => false
+  | IR GPR31 => false (* FIXME - GPR31 is used as temporary in some instructions.. ??? *)
   | IR _   => true
   | FR _   => true
   | PC     => false
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 72822f70..1edb209d 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -106,11 +106,11 @@ Definition orimm32  := opimm32 Porw  Poriw.
 Definition xorimm32 := opimm32 Pxorw Pxoriw.
 Definition sltimm32 := opimm32 Psltw Psltiw.
 Definition sltuimm32 := opimm32 Psltuw Psltiuw.
-  
+*)
 Definition load_hilo64 (r: ireg) (hi lo: int64) k :=
   if Int64.eq lo Int64.zero then Pluil r hi :: k
   else Pluil r hi :: Paddil r r lo :: k.
-  
+(*
 Definition loadimm64 (r: ireg) (n: int64) (k: code) :=
   match make_immed64 n with
   | Imm64_single imm => Paddil r GPR0 imm :: k
@@ -123,9 +123,8 @@ Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction)
                    (rd rs: ireg) (n: int64) (k: code) :=
   match make_immed64 n with
   | Imm64_single imm => opimm rd rs imm :: k
-(*| Imm64_pair hi lo => load_hilo64 GPR31 hi lo (op rd rs GPR31 :: k)
+  | Imm64_pair hi lo => load_hilo64 GPR31 hi lo (op rd rs GPR31 :: k)
   | Imm64_large imm  => Ploadli GPR31 imm :: op rd rs GPR31 :: k
-*)| _ => nil
   end.
 
 Definition addimm64 := opimm64 Paddl Paddil.
@@ -705,27 +704,19 @@ Definition transl_op
   end.
 
 (** Accessing data in the stack frame. *)
-(*
+
 Definition indexed_memory_access
         (mk_instr: ireg -> offset -> instruction)
         (base: ireg) (ofs: ptrofs) (k: code) :=
-  if Archi.ptr64 then
-    match make_immed64 (Ptrofs.to_int64 ofs) with
-    | Imm64_single imm =>
-        mk_instr base (Ofsimm (Ptrofs.of_int64 imm)) :: k
-    | Imm64_pair hi lo =>
-        Pluil GPR31 hi :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm (Ptrofs.of_int64 lo)) :: k
-    | Imm64_large imm =>
-        Ploadli GPR31 imm :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm Ptrofs.zero) :: k
-    end
-  else
-    match make_immed32 (Ptrofs.to_int ofs) with
-    | Imm32_single imm =>
-        mk_instr base (Ofsimm (Ptrofs.of_int imm)) :: k
-    | Imm32_pair hi lo =>
-        Pluiw GPR31 hi :: Paddw GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm (Ptrofs.of_int lo)) :: k
-    end.
-
+  match make_immed64 (Ptrofs.to_int64 ofs) with
+  | Imm64_single imm =>
+      mk_instr base (Ofsimm (Ptrofs.of_int64 imm)) :: k
+  | Imm64_pair hi lo =>
+      Pluil GPR31 hi :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm (Ptrofs.of_int64 lo)) :: k
+  | Imm64_large imm =>
+      Ploadli GPR31 imm :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm Ptrofs.zero) :: k
+  end.
+(*
 Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) :=
   match ty, preg_of dst with
   | Tint,    IR rd => OK (indexed_memory_access (Plw rd) base ofs k)
@@ -748,12 +739,13 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) :
   | _, _           => Error (msg "Asmgen.storeind")
   end.
 
+*)
 Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) (k: code) :=
-  indexed_memory_access (if Archi.ptr64 then Pld dst else Plw dst) base ofs k.
+  indexed_memory_access (Pld dst) base ofs k.
 
 Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) (k: code) :=
-  indexed_memory_access (if Archi.ptr64 then Psd src else Psw src) base ofs k.
-*)
+  indexed_memory_access (Psd src) base ofs k.
+
 (** Translation of memory accesses: loads, and stores. *)
 
 Definition transl_memory_access
@@ -829,9 +821,36 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing)
 
 (** Function epilogue *)
 
+(*
+Definition store_ra (base: ireg) (ofs: ptrofs) (k: code) :=
+  indexed_memory_access (Psd GPR8) base ofs (Pget GPR8 RA :: k)
+  .
+*)
+
+(*
+Definition make_ra (base: ireg) (ofs: ptrofs) (k: code) :=
+  Pset RA GPR8
+  :: (indexed_memory_access (Pld GPR8) base ofs k) (* FIXME - not sure about GPR8 *)
+  .
+*)
+
+(*
+Definition make_epilogue (f: Mach.function) (k: code) :=
+  Pset RA GPR8 :: (indexed_memory_access (Pld GPR8) SP f.(fn_retaddr_ofs) (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k))
+  (* make_ra SP f.(fn_retaddr_ofs)
+     (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k) *)
+  .
+*)
+
+Definition make_epilogue (f: Mach.function) (k: code) :=
+  Pset RA GPR8 :: loadind_ptr SP f.(fn_retaddr_ofs) GPR8
+    (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).
+
+(*
 Definition make_epilogue (f: Mach.function) (k: code) :=
   loadind_ptr SP f.(fn_retaddr_ofs) RA
     (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).
+*)
 
 (** Translation of a Mach instruction. *)
 
@@ -870,11 +889,10 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
       OK (Pj_l lbl :: k)
   | Mcond cond args lbl =>
       transl_cbranch cond args lbl k
-  | Mjumptable arg tbl =>
-      do r <- ireg_of arg;
-      OK (Pbtbl r tbl :: k)
+  | Mjumptable arg tbl => do r <- ireg_of arg; OK (Pbtbl r tbl :: k)
 *)| Mreturn =>
-      OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k))
+      OK (make_epilogue f (Pret :: k))
+      (*OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k))*)
   | _ =>
       Error (msg "Asmgen.transl_instr")
   end.
@@ -924,7 +942,16 @@ Definition transl_function (f: Mach.function) :=
   do c <- transl_code' f f.(Mach.fn_code) true;
   OK (mkfunction f.(Mach.fn_sig)
         (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
-         storeind_ptr RA SP f.(fn_retaddr_ofs) c)).
+         storeind_ptr GPR8 SP f.(fn_retaddr_ofs) (Pget GPR8 RA :: c))).
+
+(*
+Definition transl_function (f: Mach.function) :=
+  do c <- transl_code' f f.(Mach.fn_code) true;
+  OK (mkfunction f.(Mach.fn_sig)
+        (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
+         indexed_memory_access (Psd GPR8) SP f.(fn_retaddr_ofs) (Pget GPR8 RA :: c))).
+         (* store_ra SP f.(fn_retaddr_ofs) c)). *)
+*)
 
 Definition transf_function (f: Mach.function) : res Asm.function :=
   do tf <- transl_function f;
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index 0a67466a..b782608b 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -21,7 +21,7 @@ Require Import Op Locations Mach Conventions.
 Require Import Asm Asmgen Asmgenproof0.
 
 (** Decomposition of integer constants. *)
-
+(*
 Lemma make_immed32_sound:
   forall n,
   match make_immed32 n with
@@ -55,7 +55,7 @@ Proof.
   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
@@ -79,7 +79,7 @@ Qed.
 Lemma ireg_of_not_GPR31:
   forall m r, ireg_of m = OK r -> IR r <> IR GPR31.
 Proof.
-  intros. erewrite <- ireg_of_eq; eauto with asmgen. destruct m; unfold preg_of; discriminate.
+  intros. erewrite <- ireg_of_eq; eauto with asmgen.
 Qed.
 
 Lemma ireg_of_not_GPR31':
@@ -109,7 +109,7 @@ Variable ge: genv.
 Variable fn: function.
 
 (** 32-bit integer constants and arithmetic *)
-
+(*
 Lemma load_hilo32_correct:
   forall rd hi lo k rs m,
   exists rs',
@@ -175,7 +175,7 @@ Proof.
 Qed.
 
 (** 64-bit integer constants and arithmetic *)
-
+*)
 Lemma load_hilo64_correct:
   forall rd hi lo k rs m,
   exists rs',
@@ -194,7 +194,7 @@ Proof.
   split. Simpl. 
   intros; Simpl.
 Qed.
-
+(*
 Lemma loadimm64_correct:
   forall rd n k rs m,
   exists rs',
@@ -215,7 +215,7 @@ Proof.
   split. Simpl. 
   intros; Simpl.
 Qed.
-
+*)
 Lemma opimm64_correct:
   forall (op: ireg -> ireg0 -> ireg0 -> instruction)
          (opi: ireg -> ireg0 -> int64 -> instruction)
@@ -249,7 +249,7 @@ Proof.
 Qed.
 
 (** Add offset to pointer *)
-
+(*
 Lemma addptrofs_correct:
   forall rd r1 n k rs m,
   r1 <> GPR31 ->
@@ -385,7 +385,7 @@ Remark branch_on_GPR31:
 Proof.
   intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. 
 Qed.
-
+*)
 Ltac ArgsInv :=
   repeat (match goal with
   | [ H: Error _ = OK _ |- _ ] => discriminate
@@ -415,7 +415,7 @@ Remark exec_straight_opt_right:
 Proof.
   destruct 1; intros. auto. eapply exec_straight_trans; eauto. 
 Qed.
-
+(*
 Lemma transl_cbranch_correct_1:
   forall cond args lbl k c m ms b sp rs m',
   transl_cbranch cond args lbl k = OK c ->
@@ -940,7 +940,7 @@ Proof.
   apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto.
   split; intros; Simpl.
 Qed.
-
+*)
 (** Some arithmetic properties. *)
 
 Remark cast32unsigned_from_cast32signed:
@@ -980,6 +980,7 @@ Proof.
 Opaque Int.eq.
   intros until c; intros TR EV.
   unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl.
+(*
 - (* move *)
   destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl.
 - (* intconst *)
@@ -1069,10 +1070,12 @@ Opaque Int.eq.
   assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto.
   rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal.
   rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto.
+*)
 - (* addlimm *)
   exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
-  exists rs'; split; eauto. rewrite B; auto with asmgen. 
+  exists rs'; split; eauto. rewrite B; auto with asmgen.
+(*
 - (* andimm *)
   exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
@@ -1100,6 +1103,7 @@ Opaque Int.eq.
 - (* cond *)
   exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
   exists rs'; split. eexact A. eauto with asmgen.
+*)
 Qed.
 
 (** Memory accesses *)
@@ -1114,7 +1118,8 @@ Lemma indexed_memory_access_correct:
   /\ forall r, r <> PC -> r <> GPR31 -> rs'#r = rs#r.
 Proof.
   unfold indexed_memory_access; intros.
-  destruct Archi.ptr64 eqn:SF.
+  (* destruct Archi.ptr64 eqn:SF. *)
+  assert (Archi.ptr64 = true) as SF; auto.
 - generalize (make_immed64_sound (Ptrofs.to_int64 ofs)); intros EQ.
   destruct (make_immed64 (Ptrofs.to_int64 ofs)).
 + econstructor; econstructor; econstructor; split.
@@ -1132,6 +1137,7 @@ Proof.
   simpl; eauto. simpl; eauto. auto. auto. 
   split; intros; Simpl. unfold eval_offset. destruct (rs base); auto; simpl. rewrite SF. simpl.
   rewrite Ptrofs.add_zero. subst imm. rewrite Ptrofs.of_int64_to_int64 by auto. auto.
+(* 32 bits part, irrelevant for us
 - generalize (make_immed32_sound (Ptrofs.to_int ofs)); intros EQ.
   destruct (make_immed32 (Ptrofs.to_int ofs)).
 + econstructor; econstructor; econstructor; split.
@@ -1144,6 +1150,7 @@ Proof.
   rewrite Ptrofs.add_assoc. f_equal. f_equal. 
   rewrite <- (Ptrofs.of_int_to_int SF ofs). rewrite EQ. 
   symmetry; auto with ptrofs.
+*)
 Qed.
 
 Lemma indexed_load_access_correct:
@@ -1186,7 +1193,7 @@ Proof.
   unfold exec_store. rewrite B, C, STORE by auto. eauto. auto. 
   intros; Simpl.
 Qed.
-
+(*
 Lemma loadind_correct:
   forall (base: ireg) ofs ty dst k c (rs: regset) m v,
   loadind base ofs ty dst k = OK c ->
@@ -1227,7 +1234,7 @@ Proof.
   destruct A as (mk_instr & B & C). subst c. 
   eapply indexed_store_access_correct; eauto with asmgen. 
 Qed.
-
+*)
 Lemma loadind_ptr_correct:
   forall (base: ireg) ofs (dst: ireg) k (rs: regset) m v,
   Mem.loadv Mptr m (Val.offset_ptr rs#base ofs) = Some v ->
@@ -1238,9 +1245,9 @@ Lemma loadind_ptr_correct:
   /\ forall r, r <> PC -> r <> GPR31 -> r <> dst -> rs'#r = rs#r.
 Proof.
   intros. eapply indexed_load_access_correct; eauto with asmgen.
-  intros. unfold Mptr. destruct Archi.ptr64; auto. 
+  intros. unfold Mptr. assert (Archi.ptr64 = true). auto. rewrite H1. auto.
 Qed.
-
+(*
 Lemma storeind_ptr_correct:
   forall (base: ireg) ofs (src: ireg) k (rs: regset) m m',
   Mem.storev Mptr m (Val.offset_ptr rs#base ofs) rs#src = Some m' ->
@@ -1252,7 +1259,7 @@ Proof.
   intros. eapply indexed_store_access_correct with (r1 := src); eauto with asmgen.
   intros. unfold Mptr. destruct Archi.ptr64; auto. 
 Qed.
-
+*)
 Lemma transl_memory_access_correct:
   forall mk_instr addr args k c (rs: regset) m v,
   transl_memory_access mk_instr addr args k = OK c ->
@@ -1264,6 +1271,7 @@ Lemma transl_memory_access_correct:
 Proof.
   intros until v; intros TR EV. 
   unfold transl_memory_access in TR; destruct addr; ArgsInv.
+(*
 - (* indexed *)
   inv EV. apply indexed_memory_access_correct; eauto with asmgen.
 - (* global *)
@@ -1272,6 +1280,7 @@ Proof.
   split; intros; Simpl. unfold eval_offset. apply low_high_half.
 - (* stack *)
   inv TR. inv EV. apply indexed_memory_access_correct; eauto with asmgen.
+*)
 Qed.
 
 Lemma transl_load_access_correct:
@@ -1354,16 +1363,16 @@ Proof.
    /\ 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;
     (econstructor; econstructor; 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 as (mk_instr & chunk' & B & C & D).
   rewrite D in STORE; clear D. 
   eapply transl_store_access_correct; eauto with asmgen.
 Qed.
 
-(** Function epilogues *)
-
 Lemma make_epilogue_correct:
   forall ge0 f m stk soff cs m' ms rs k tm,
   load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) ->
@@ -1387,7 +1396,8 @@ Proof.
   exploit lessdef_parent_ra; eauto. intros EQ; subst ra'; clear LDRA'.
   exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT').
   unfold make_epilogue. 
-  rewrite chunk_of_Tptr in *. 
+  rewrite chunk_of_Tptr in *.
+  
   exploit (loadind_ptr_correct SP (fn_retaddr_ofs f) RA (Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: k) rs tm).
     rewrite <- (sp_val _ _ _ AG). simpl. eexact LRA'. congruence.
   intros (rs1 & A1 & B1 & C1).