MPPA - bunch of ops added : lowlong, and, or, shr..

mppa_k1c/Asm.v

@@ -191,18 +191,29 @@ Inductive instruction : Type :=
 
 (** 32-bit integer register-immediate instructions *)
   | Paddiw  (rd: ireg) (rs: ireg) (imm: int)        (**r add immediate *)
+  | Pandiw  (rd: ireg) (rs: ireg) (imm: int)        (**r and immediate *)
+  | Psrliw  (rd: ireg) (rs: ireg) (imm: int)        (**r shift right logical immediate *)
 
 (** 32-bit integer register-register instructions *)
   | Paddw   (rd: ireg) (rs1 rs2: ireg)              (**r integer addition *)
+  | Pandw   (rd: ireg) (rs1 rs2: ireg)              (**r integer andition *)
   | Pnegw   (rd: ireg) (rs: ireg)                   (**r negate word *)
 
 (** 64-bit integer register-immediate instructions *)
   | Paddil  (rd: ireg) (rs: ireg) (imm: int64)      (**r add immediate *) 
+  | Pandil  (rd: ireg) (rs: ireg) (imm: int64)      (**r and immediate *) 
+  | Poril   (rd: ireg) (rs: ireg) (imm: int64)      (**r or long immediate *) 
+  | Psrlil  (rd: ireg) (rs: ireg) (imm: int)        (**r shift right logical immediate long *)
   | Pmake   (rd: ireg)            (imm: int)        (**r load immediate *)
   | Pmakel  (rd: ireg)            (imm: int64)      (**r load immediate long *)
 
+(** Conversions *)
+  | Pcvtl2w (rd: ireg) (rs: ireg)                   (**r Convert Long to Word *)
+
 (** 64-bit integer register-register instructions *)
   | Paddl   (rd: ireg) (rs1 rs2: ireg)              (**r integer addition *)
+  | Pandl   (rd: ireg) (rs1 rs2: ireg)              (**r integer andition *)
+  | Porl    (rd: ireg) (rs1 rs2: ireg)              (**r or long *)
   | Pnegl   (rd: ireg) (rs: ireg)                   (**r negate long *)
 
   (* Unconditional jumps.  Links are always to X1/RA. *)
@@ -713,16 +724,28 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
 (** 32-bit integer register-immediate instructions *)
   | Paddiw d s i =>
       Next (nextinstr (rs#d <- (Val.add rs##s (Vint i)))) m
+  | Pandiw d s i =>
+      Next (nextinstr (rs#d <- (Val.and rs##s (Vint i)))) m
+  | Psrliw d s i =>
+      Next (nextinstr (rs#d <- (Val.shru rs##s (Vint i)))) m
 
 (** 32-bit integer register-register instructions *)
   | Paddw d s1 s2 =>
       Next (nextinstr (rs#d <- (Val.add rs##s1 rs##s2))) m
+  | Pandw d s1 s2 =>
+      Next (nextinstr (rs#d <- (Val.and rs##s1 rs##s2))) m
   | Pnegw d s =>
       Next (nextinstr (rs#d <- (Val.neg rs###s))) m
 
 (** 64-bit integer register-immediate instructions *)
   | Paddil d s i =>
       Next (nextinstr (rs#d <- (Val.addl rs###s (Vlong i)))) m
+  | Pandil d s i =>
+      Next (nextinstr (rs#d <- (Val.andl rs###s (Vlong i)))) m
+  | Poril  d s i =>
+      Next (nextinstr (rs#d <- (Val.orl  rs###s (Vlong i)))) m
+  | Psrlil  d s i =>
+      Next (nextinstr (rs#d <- (Val.shrlu  rs###s (Vint i)))) m
   | Pmakel d i =>
       Next (nextinstr (rs#d <- (Vlong i))) m
   | Pmake d i =>
@@ -731,9 +754,17 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
 (** 64-bit integer register-register instructions *)
   | Paddl d s1 s2 =>
       Next (nextinstr (rs#d <- (Val.addl rs###s1 rs###s2))) m
+  | Pandl d s1 s2 =>
+      Next (nextinstr (rs#d <- (Val.andl rs###s1 rs###s2))) m
+  | Porl  d s1 s2 =>
+      Next (nextinstr (rs#d <- (Val.orl  rs###s1 rs###s2))) m
   | Pnegl d s =>
       Next (nextinstr (rs#d <- (Val.negl rs###s))) m
 
+(** Conversions *)
+  | Pcvtl2w d s =>
+      Next (nextinstr (rs#d <- (Val.loword rs###s))) m
+
 (** Unconditional jumps. *)
   | Pj_l l =>
       goto_label f l rs m

mppa_k1c/Asmexpand.ml

@@ -548,10 +548,10 @@ let expand_instruction instr =
       end else begin
         emit (Pxorl(rd, rs1, rs2)); emit (Psltul(rd, X0, X rd))
       end
-  | Pcvtl2w(rd, rs) ->
+*)| Pcvtl2w(rd, rs) ->
       assert Archi.ptr64;
       emit (Paddiw(rd, rs, Int.zero))  (* 32-bit sign extension *)
-  | Pcvtw2l(r) ->
+(*| Pcvtw2l(r) ->
       assert Archi.ptr64
       (* no-operation because the 32-bit integer was kept sign extended already *)
 

mppa_k1c/Asmgen.v

@@ -82,8 +82,8 @@ Definition opimm32 (op: ireg -> ireg -> ireg -> instruction)
   end.
 
 Definition addimm32 := opimm32 Paddw Paddiw.
-(*
 Definition andimm32 := opimm32 Pandw Pandiw.
+(*
 Definition orimm32  := opimm32 Porw  Poriw.
 Definition xorimm32 := opimm32 Pxorw Pxoriw.
 Definition sltimm32 := opimm32 Psltw Psltiw.
@@ -107,10 +107,10 @@ Definition opimm64 (op: ireg -> ireg -> ireg -> instruction)
 end.
 
 Definition addimm64 := opimm64 Paddl Paddil.
+Definition orimm64  := opimm64 Porl  Poril.
+Definition andimm64 := opimm64 Pandl Pandil.
 
 (*
-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.
@@ -286,10 +286,10 @@ Definition transl_op
   | Oand, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pandw rd rs1 rs2 :: k)
-  | Oandimm n, a1 :: nil =>
+*)| Oandimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (andimm32 rd rs n k)
-  | Oor, a1 :: a2 :: nil =>
+(*| Oor, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Porw rd rs1 rs2 :: k)
   | Oorimm n, a1 :: nil =>
@@ -316,10 +316,10 @@ Definition transl_op
   | Oshru, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Psrlw rd rs1 rs2 :: k)
-  | Oshruimm n, a1 :: nil =>
+*)| Oshruimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (Psrliw rd rs n :: k)
-  | Oshrximm n, a1 :: nil =>
+(*| Oshrximm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (if Int.eq n Int.zero then Pmv rd rs :: k else
           Psraiw GPR31 rs (Int.repr 31) ::
@@ -328,10 +328,10 @@ Definition transl_op
           Psraiw rd GPR31 n :: k)
 
   (* [Omakelong], [Ohighlong]  should not occur *)
-  | Olowlong, a1 :: nil =>
+*)| Olowlong, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (Pcvtl2w rd rs :: k)  
-  | Ocast32signed, a1 :: nil =>
+(*| Ocast32signed, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       assertion (ireg_eq rd rs);
       OK (Pcvtw2l rd :: k)
@@ -375,16 +375,16 @@ Definition transl_op
   | Oandl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pandl rd rs1 rs2 :: k)
-  | Oandlimm n, a1 :: nil =>
+*)| Oandlimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (andimm64 rd rs n k)
-  | Oorl, a1 :: a2 :: nil =>
+(*| Oorl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Porl rd rs1 rs2 :: k)
-  | Oorlimm n, a1 :: nil =>
+*)| Oorlimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (orimm64 rd rs n k)
-  | Oxorl, a1 :: a2 :: nil =>
+(*| Oxorl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pxorl rd rs1 rs2 :: k)
   | Oxorlimm n, a1 :: nil =>
@@ -405,10 +405,10 @@ Definition transl_op
   | Oshrlu, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Psrll rd rs1 rs2 :: k)
-  | Oshrluimm n, a1 :: nil =>
+*)| Oshrluimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (Psrlil rd rs n :: k)
-  | Oshrxlimm n, a1 :: nil =>
+(*| Oshrxlimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (if Int.eq n Int.zero then Pmv rd rs :: k else
           Psrail GPR31 rs (Int.repr 63) ::
@@ -656,9 +656,9 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
                 else loadind_ptr SP f.(fn_link_ofs) GPR30 c)
 *)| Mop op args res =>
       transl_op op args res k
-(*| Mload chunk addr args dst =>
+  | Mload chunk addr args dst =>
       transl_load chunk addr args dst k
-  | Mstore chunk addr args src =>
+(*| Mstore chunk addr args src =>
       transl_store chunk addr args src k
   | Mcall sig (inl r) =>
       do r1 <- ireg_of r; OK (Pjal_r r1 sig :: k)

mppa_k1c/Asmgenproof.v

@@ -307,8 +307,14 @@ Opaque Int.eq.
 - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
 (* Oaddimm32 *)
 - apply opimm32_label; intros; exact I.
+(* Oandimm32 *)
+- apply opimm32_label; intros; exact I.
 (* Oaddimm64 *)
 - apply opimm64_label; intros; exact I.
+(* Oandimm64  *)
+- apply opimm64_label; intros; exact I.
+(* Oorimm64  *)
+- apply opimm64_label; intros; exact I.
 Qed.
 
 (*

mppa_k1c/TargetPrinter.ml

@@ -211,12 +211,33 @@ module Target : TARGET =
          fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Paddil (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Paddl(rd, rs1, rs2) -> assert Archi.ptr64;
+         fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+
+      | Psrliw (rd, rs, imm) ->
+         fprintf oc "	srlw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Psrlil (rd, rs, imm) ->
+         fprintf oc "	srld	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+
+      | Poril (rd, rs, imm) -> assert Archi.ptr64;
+         fprintf oc "	ord	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Porl(rd, rs1, rs2) -> assert Archi.ptr64;
+         fprintf oc "	ord	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+
+      | Pandiw (rd, rs, imm) ->
+         fprintf oc "	andd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Pandw(rd, rs1, rs2) ->
+         fprintf oc "	andd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Pandil (rd, rs, imm) -> assert Archi.ptr64;
+         fprintf oc "	andd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Pandl(rd, rs1, rs2) -> assert Archi.ptr64;
+         fprintf oc "	andd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+
       | Pmake (rd, imm) ->
          fprintf oc "	make	%a, %a\n;;\n" ireg rd coqint imm
       | Pmakel (rd, imm) ->
          fprintf oc "	make	%a, %a\n;;\n" ireg rd coqint64 imm
-      | Paddl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+
       | Pnegl(rd, rs) -> assert Archi.ptr64;
          fprintf oc "	negd	%a = %a\n;;\n" ireg rd ireg rs
       | Pnegw(rd, rs) ->
@@ -243,6 +264,7 @@ module Target : TARGET =
          assert false
       | Pfreeframe(sz, ofs) ->
          assert false
+      | Pcvtl2w _ -> assert false
 
       (* Pseudo-instructions that remain *)
       | Plabel lbl ->