Merge remote-tracking branch 'origin/kvx-bits' into kvx_fp_division

1 files changed, 13 insertions, 1 deletions

diff --git a/kvx/Asmblockgen.v b/kvx/Asmblockgen.v
index a8f1a045..07b31b11 100644
--- a/kvx/Asmblockgen.v
+++ b/kvx/Asmblockgen.v
@@ -535,6 +535,12 @@ Definition transl_op
   | Oornimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (Porniw rd rs n ::i k)
+  | Oabsdiff, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pabdw rd rs1 rs2 ::i k)
+  | Oabsdiffimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Pabdiw rd rs n ::i k)
   | Oshl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Psllw rd rs1 rs2 ::i k)
@@ -672,6 +678,12 @@ Definition transl_op
   | Oornlimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (Pornil rd rs n ::i k)
+  | Oabsdiffl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pabdl rd rs1 rs2 ::i k)
+  | Oabsdifflimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Pabdil rd rs n ::i k)
   | Oshll, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pslll rd rs1 rs2 ::i k)
@@ -901,7 +913,7 @@ Definition transl_op
       do rC <- ireg_of aC;
       do op <- conditional_move_imm64 (negate_condition0 cond0) rC rT imm;
       OK (op ::i k)
-      
+         
   | _, _ =>
       Error(msg "Asmgenblock.transl_op")
   end.