orn / andn in asm

4 files changed, 50 insertions, 4 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index e07b1190..8486e25d 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -284,6 +284,8 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRR Asmblock.Pnorw rd rs1 rs2       => Pnorw rd rs1 rs2

   | PArithRRR Asmblock.Pxorw rd rs1 rs2       => Pxorw rd rs1 rs2

   | PArithRRR Asmblock.Pnxorw rd rs1 rs2      => Pnxorw rd rs1 rs2

+  | PArithRRR Asmblock.Pandnw rd rs1 rs2      => Pandnw rd rs1 rs2

+  | PArithRRR Asmblock.Pornw rd rs1 rs2       => Pornw rd rs1 rs2

   | PArithRRR Asmblock.Psraw rd rs1 rs2       => Psraw rd rs1 rs2

   | PArithRRR Asmblock.Psrlw rd rs1 rs2       => Psrlw rd rs1 rs2

   | PArithRRR Asmblock.Psllw rd rs1 rs2       => Psllw rd rs1 rs2

@@ -296,6 +298,8 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRR Asmblock.Pnorl rd rs1 rs2       => Pnorl rd rs1 rs2

   | PArithRRR Asmblock.Pxorl rd rs1 rs2       => Pxorl rd rs1 rs2

   | PArithRRR Asmblock.Pnxorl rd rs1 rs2      => Pnxorl rd rs1 rs2

+  | PArithRRR Asmblock.Pandnl rd rs1 rs2      => Pandnl rd rs1 rs2

+  | PArithRRR Asmblock.Pornl rd rs1 rs2       => Pornl rd rs1 rs2

   | PArithRRR Asmblock.Pmull rd rs1 rs2       => Pmull rd rs1 rs2

   | PArithRRR Asmblock.Pslll rd rs1 rs2       => Pslll rd rs1 rs2

   | PArithRRR Asmblock.Psrll rd rs1 rs2       => Psrll rd rs1 rs2

@@ -317,6 +321,8 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRI32 Asmblock.Pnoriw rd rs imm       => Pnoriw rd rs imm

   | PArithRRI32 Asmblock.Pxoriw rd rs imm       => Pxoriw rd rs imm

   | PArithRRI32 Asmblock.Pnxoriw rd rs imm      => Pnxoriw rd rs imm

+  | PArithRRI32 Asmblock.Pandniw rd rs imm      => Pandniw rd rs imm

+  | PArithRRI32 Asmblock.Porniw rd rs imm       => Porniw rd rs imm

   | PArithRRI32 Asmblock.Psraiw rd rs imm       => Psraiw rd rs imm

   | PArithRRI32 Asmblock.Psrliw rd rs imm       => Psrliw rd rs imm

   | PArithRRI32 Asmblock.Pslliw rd rs imm       => Pslliw rd rs imm

@@ -334,6 +340,8 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRI64 Asmblock.Pnoril rd rs imm       => Pnoril rd rs imm

   | PArithRRI64 Asmblock.Pxoril rd rs imm       => Pxoril rd rs imm

   | PArithRRI64 Asmblock.Pnxoril rd rs imm      => Pnxoril rd rs imm

+  | PArithRRI64 Asmblock.Pandnil rd rs imm      => Pandnil rd rs imm

+  | PArithRRI64 Asmblock.Pornil rd rs imm       => Pornil rd rs imm

 

   (** Load *)

   | PLoadRRO Asmblock.Plb rd ra ofs   => Plb rd ra ofs

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 5279bd29..cdbe4eb3 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -343,6 +343,8 @@ Inductive arith_name_rrr : Type :=
   | Pnorw                                           (**r nor word *)
   | Pxorw                                           (**r xor word *)
   | Pnxorw                                          (**r nxor word *)
+  | Pandnw                                          (**r andn word *)
+  | Pornw                                           (**r orn word *)
   | Psraw                                           (**r shift right arithmetic word *)
   | Psrlw                                           (**r shift right logical word *)
   | Psllw                                           (**r shift left logical word *)
@@ -355,6 +357,8 @@ Inductive arith_name_rrr : Type :=
   | Pnorl                                           (**r nor long *)
   | Pxorl                                           (**r xor long *)
   | Pnxorl                                          (**r nxor long *)
+  | Pandnl                                          (**r andn long *)
+  | Pornl                                           (**r orn long *)
   | Pmull                                           (**r mul long (low part) *)
   | Pslll                                           (**r shift left logical long *)
   | Psrll                                           (**r shift right logical long *)
@@ -378,6 +382,8 @@ Inductive arith_name_rri32 : Type :=
   | Pnoriw                                          (**r nor imm word *)
   | Pxoriw                                          (**r xor imm word *)
   | Pnxoriw                                         (**r nxor imm word *)
+  | Pandniw                                         (**r andn word *)
+  | Porniw                                          (**r orn word *)
   | Psraiw                                          (**r shift right arithmetic imm word *)
   | Psrliw                                          (**r shift right logical imm word *)
   | Pslliw                                          (**r shift left logical imm word *)
@@ -396,6 +402,8 @@ Inductive arith_name_rri64 : Type :=
   | Pnoril                                          (**r nor immediate long *) 
   | Pxoril                                          (**r xor immediate long *) 
   | Pnxoril                                         (**r nxor immediate long *) 
+  | Pandnil                                         (**r andn immediate long *)
+  | Pornil                                          (**r orn immediate long *)
 .
 
 Inductive ar_instruction : Type :=
@@ -1108,6 +1116,8 @@ Definition arith_eval_rrr n v1 v2 :=
   | Pnorw  => Val.notint (Val.or v1 v2)
   | Pxorw  => Val.xor  v1 v2
   | Pnxorw => Val.notint (Val.xor v1 v2)
+  | Pandnw => Val.and (Val.notint v1) v2
+  | Pornw  => Val.or (Val.notint v1) v2
   | Psrlw  => Val.shru v1 v2
   | Psraw  => Val.shr  v1 v2
   | Psllw  => Val.shl  v1 v2
@@ -1120,6 +1130,8 @@ Definition arith_eval_rrr n v1 v2 :=
   | Pnorl  => Val.notl (Val.orl  v1 v2)
   | Pxorl  => Val.xorl  v1 v2
   | Pnxorl  => Val.notl (Val.xorl  v1 v2)
+  | Pandnl => Val.andl (Val.notl v1) v2
+  | Pornl  => Val.orl (Val.notl v1) v2
   | Pmull => Val.mull v1 v2
   | Pslll => Val.shll v1 v2
   | Psrll => Val.shrlu v1 v2
@@ -1143,6 +1155,8 @@ Definition arith_eval_rri32 n v i :=
   | Pnoriw  => Val.notint (Val.or v (Vint i))
   | Pxoriw  => Val.xor   v (Vint i)
   | Pnxoriw => Val.notint (Val.xor v (Vint i))
+  | Pandniw => Val.and (Val.notint v) (Vint i)
+  | Porniw  => Val.or (Val.notint v) (Vint i)
   | Psraiw  => Val.shr   v (Vint i)
   | Psrliw  => Val.shru  v (Vint i)
   | Pslliw  => Val.shl   v (Vint i)
@@ -1162,6 +1176,8 @@ Definition arith_eval_rri64 n v i :=
   | Pnoril   => Val.notl (Val.orl  v (Vlong i))
   | Pxoril  => Val.xorl  v (Vlong i)
   | Pnxoril  => Val.notl (Val.xorl  v (Vlong i))
+  | Pandnil => Val.andl (Val.notl v) (Vlong i)
+  | Pornil  => Val.orl (Val.notl v) (Vlong i)
   end.
 
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index c5b5bd56..d69903b4 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1305,6 +1305,8 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
   | Pnorw => "Pnorw"
   | Pxorw => "Pxorw"
   | Pnxorw => "Pnxorw"
+  | Pandnw => "Pandnw"
+  | Pornw => "Pornw"
   | Psraw => "Psraw"
   | Psrlw => "Psrlw"
   | Psllw => "Psllw"
@@ -1316,6 +1318,8 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
   | Pnorl => "Pnorl"
   | Pxorl => "Pxorl"
   | Pnxorl => "Pnxorl"
+  | Pandnl => "Pandnl"
+  | Pornl => "Pornl"
   | Pmull => "Pmull"
   | Pslll => "Pslll"
   | Psrll => "Psrll"
@@ -1338,6 +1342,8 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
   | Pnoriw => "Pnoriw"
   | Pxoriw => "Pxoriw"
   | Pnxoriw => "Pnxoriw"
+  | Pandniw => "Pandniw"
+  | Porniw => "Porniw"
   | Psraiw => "Psraiw"
   | Psrliw => "Psrliw"
   | Pslliw => "Pslliw"
@@ -1357,6 +1363,8 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring :=
   | Pnoril => "Pnoril"
   | Pxoril => "Pxoril"
   | Pnxoril => "Pnxoril"
+  | Pandnil => "Pandnil"
+  | Pornil => "Pornil"
   end.
 
 Definition string_of_arith (op: arith_op): pstring :=
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 3c242441..ce2fb2ae 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -66,6 +66,8 @@ let arith_rrr_str = function
   | Pnorw -> "Pnorw"
   | Pxorw -> "Pxorw"
   | Pnxorw -> "Pnxorw"
+  | Pandnw -> "Pandnw"
+  | Pornw -> "Pornw"
   | Psraw -> "Psraw"
   | Psrlw -> "Psrlw"
   | Psllw -> "Psllw"
@@ -77,6 +79,8 @@ let arith_rrr_str = function
   | Pnorl -> "Pnorl"
   | Pxorl -> "Pxorl"
   | Pnxorl -> "Pnxorl"
+  | Pandnl -> "Pandnl"
+  | Pornl -> "Pornl"
   | Pmull -> "Pmull"
   | Pslll -> "Pslll"
   | Psrll -> "Psrll"
@@ -97,6 +101,8 @@ let arith_rri32_str = function
   | Pnoriw -> "Pnoriw"
   | Pxoriw -> "Pxoriw"
   | Pnxoriw -> "Pnxoriw"
+  | Pandniw -> "Pandniw"
+  | Porniw -> "Porniw"
   | Psraiw -> "Psraiw"
   | Psrliw -> "Psrliw"
   | Pslliw -> "Pslliw"
@@ -114,6 +120,8 @@ let arith_rri64_str = function
   | Pnoril -> "Pnoril"
   | Pxoril -> "Pxoril"
   | Pnxoril -> "Pnxoril"
+  | Pandnil -> "Pandnil"
+  | Pornil -> "Pornil"
 
 let arith_ri32_str = "Pmake"
 
@@ -390,7 +398,7 @@ type real_instruction =
   (* ALU *) 
   | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw
   | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord
-  | Nandw | Norw | Nxorw | Nandd | Nord | Nxord                                                      
+  | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd
   | Make | Nop  | Sxwd  | Zxwd
   (* LSU *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld
@@ -431,8 +439,12 @@ let ab_inst_to_real = function
   | "Pslll" | "Psllil" -> Slld
   | "Pxorw" | "Pxoriw" -> Xorw
   | "Pnxorw" | "Pnxoriw" -> Nxorw
+  | "Pandnw" | "Pandniw" -> Andnw
+  | "Pornw" | "Porniw" -> Ornw
   | "Pxorl" | "Pxoril" -> Xord
   | "Pnxorl" | "Pnxoril" -> Nxord
+  | "Pandnl" | "Pandnil" -> Andnd
+  | "Pornl" | "Pornil" -> Ornd
   | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make
   | "Pnop" | "Pcvtw2l" -> Nop
   | "Psxwd" -> Sxwd
@@ -494,11 +506,11 @@ let rec_to_usage r =
                                   (* I do not know yet in which context Ofslow can be used by CompCert *)
   and real_inst = ab_inst_to_real r.inst
   in match real_inst with
-  | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw | Nxorw -> 
+  | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw | Nxorw | Andnw | Ornw -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | _ -> raise InvalidEncoding)
-  | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord | Nxord -> 
+  | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord | Nxord | Andnd | Ornd -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | Some E27U27L10 -> alu_tiny_y)
@@ -547,7 +559,9 @@ let rec_to_usage r =
 let real_inst_to_latency = function
   | Nop -> 0 (* Only goes through ID *)
   | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw
-  | Rorw | Nandw | Norw | Nxorw | Nandd | Nord | Nxord
+    (* TODO check rorw *)
+  | Rorw | Nandw | Norw | Nxorw | Ornw | Andnw
+  | Nandd | Nord | Nxord | Ornd | Andnd
   | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
   | Sxwd | Zxwd | Fcompw | Fcompd
         -> 1