MPPA - Removed Plui, replaced with Pmake, and modified make_immed64

4 files changed, 40 insertions, 27 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 22b2c7a3..5c8a6360 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -138,11 +138,11 @@ Inductive instruction : Type :=
   | 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 *)
 
 (** 32-bit integer register-immediate instructions *)
-  | Paddiw  (rd: ireg) (rs: ireg0) (imm: int)        (**r add immediate *)
+(*| Paddiw  (rd: ireg) (rs: ireg0) (imm: int)        (**r add immediate *)
   | Psltiw  (rd: ireg) (rs: ireg0) (imm: int)        (**r set-less-than immediate *)
   | Psltiuw (rd: ireg) (rs: ireg0) (imm: int)        (**r set-less-than unsigned immediate *)
   | Pandiw  (rd: ireg) (rs: ireg0) (imm: int)        (**r and immediate *)
@@ -184,7 +184,8 @@ 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 FIXME - remove it ; load upper-immediate *)
+*)| Pmake   (rd: ireg)             (imm: int64)      (**r load immediate *)
 (** 64-bit integer register-register instructions *)
   | Paddl   (rd: ireg) (rs1 rs2: ireg0)              (**r integer addition *) (*
   | Psubl   (rd: ireg) (rs1 rs2: ireg0)              (**r integer subtraction *)
@@ -634,11 +635,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
     end
   | Pret =>
       Next (rs#PC <- (rs#RA)) m
-(*  | Pmv d s =>
+  | Pmv d s =>
       Next (nextinstr (rs#d <- (rs#s))) m
 
 (** 32-bit integer register-immediate instructions *)
-  | Paddiw d s i =>
+(*| Paddiw d s i =>
       Next (nextinstr (rs#d <- (Val.add rs##s (Vint i)))) m
   | Psltiw d s i =>
       Next (nextinstr (rs#d <- (Val.cmp Clt rs##s (Vint i)))) m
@@ -718,8 +719,10 @@ 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
+*)| Pmake d i =>
+      Next (nextinstr (rs#d <- (Vlong i))) m
 
 (** 64-bit integer register-register instructions *)
   | Paddl d s1 s2 =>
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index c8ea4279..e1c01d3f 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -65,16 +65,19 @@ Definition make_immed32 (val: int) :=
 *)
 Inductive immed64 : Type :=
   | Imm64_single (imm: int64)
-  | Imm64_pair   (hi: int64) (lo: int64)
+(*| Imm64_pair   (hi: int64) (lo: int64)
   | Imm64_large  (imm: int64).
+*).
 
-Definition make_immed64 (val: int64) :=
-  let lo := Int64.sign_ext 12 val in
+(* For now, let's suppose all instructions of K1c can handle 64-bits immediate *)
+Definition make_immed64 (val: int64) := Imm64_single val.
+(*let lo := Int64.sign_ext 12 val in
   if Int64.eq val lo then Imm64_single lo else
   let hi := Int64.zero_ext 20 (Int64.shru (Int64.sub val lo) (Int64.repr 12)) in
   if Int64.eq val (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo)
   then Imm64_pair hi lo
   else Imm64_large val.
+*)
 (*
 (** Smart constructors for arithmetic operations involving
   a 32-bit or 64-bit integer constant.  Depending on whether the
@@ -107,9 +110,11 @@ 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
@@ -123,26 +128,27 @@ 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
-  end.
+*)end.
 
 Definition addimm64 := opimm64 Paddl Paddil.
+
 (*
 Definition andimm64 := opimm64 Pandl Pandil.
 Definition orimm64  := opimm64 Porl  Poril.
 Definition xorimm64 := opimm64 Pxorl  Pxoril.
 Definition sltimm64 := opimm64 Psltl Psltil.
 Definition sltuimm64 := opimm64 Psltul Psltiul.
+*)
 
 Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   if Ptrofs.eq_dec n Ptrofs.zero then
     Pmv rd rs :: k
   else
-    if Archi.ptr64
-    then addimm64 rd rs (Ptrofs.to_int64 n) k
-    else addimm32 rd rs (Ptrofs.to_int n) k.
-  
+    addimm64 rd rs (Ptrofs.to_int64 n) k.
+
+(*
 (** Translation of conditional branches. *)
 
 Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
@@ -711,11 +717,11 @@ Definition indexed_memory_access
   match make_immed64 (Ptrofs.to_int64 ofs) with
   | Imm64_single imm =>
       mk_instr base (Ofsimm (Ptrofs.of_int64 imm)) :: k
-  | Imm64_pair hi lo =>
+(*| 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.
+      Pmake 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
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 51d093f8..568311f5 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -149,7 +149,7 @@ Remark opimm64_label:
   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.
+(*unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.*)
 Qed.
 Hint Resolve opimm64_label: labels.
 (*
@@ -414,7 +414,8 @@ Lemma transl_find_label:
 Proof.
   intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
   monadInv EQ. rewrite transl_code'_transl_code in EQ0. unfold fn_code. 
-  simpl. destruct (storeind_ptr_label GPR8 GPR12 (fn_retaddr_ofs f) x) as [A B]; rewrite B. 
+  simpl. destruct (storeind_ptr_label GPR8 GPR12 (fn_retaddr_ofs f) x) as [A B]. 
+  (* destruct B. *)
   eapply transl_code_label; eauto.
 Qed.
 
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index c712b5e7..f83275a1 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -60,9 +60,9 @@ 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_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.
@@ -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',
@@ -236,6 +236,7 @@ Proof.
 - subst imm. econstructor; split. 
   apply exec_straight_one. rewrite H0. simpl; eauto. auto.
   split. Simpl. intros; Simpl.
+(*
 - destruct (load_hilo64_correct GPR31 hi lo (op rd r1 GPR31 :: k) rs m)
   as (rs' & A & B & C).
   econstructor; split.
@@ -246,6 +247,7 @@ Proof.
 - subst imm. econstructor; split. 
   eapply exec_straight_two. simpl; eauto. rewrite H. simpl; eauto. auto. auto.
   split. Simpl. intros; Simpl.
+*)
 Qed.
 
 (** Add offset to pointer *)
@@ -1070,12 +1072,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.
-(*
+  
 - (* andimm *)
   exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen.
   intros (rs' & A & B & C).
@@ -1125,6 +1127,7 @@ Proof.
 + econstructor; econstructor; econstructor; split.
   apply exec_straight_opt_refl. 
   split; auto. simpl. subst imm. rewrite Ptrofs.of_int64_to_int64 by auto. auto.
+(*
 + econstructor; econstructor; econstructor; split. 
   constructor. eapply exec_straight_two. 
   simpl; eauto. simpl; eauto. auto. auto. 
@@ -1150,7 +1153,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: