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

17 files changed, 374 insertions, 18 deletions

diff --git a/kvx/Asm.v b/kvx/Asm.v
index 333854cf..7a289fe5 100644
--- a/kvx/Asm.v
+++ b/kvx/Asm.v
@@ -251,6 +251,9 @@ Inductive instruction : Type :=
   | Pfmaxd              (rd rs1 rs2: ireg)          (**r Float max double *)
   | Pfmaxw              (rd rs1 rs2: ireg)          (**r Float max word *)
   | Pfinvw              (rd rs1: ireg)              (**r Float invert word *)
+
+  | Pabdw               (rd rs1 rs2: ireg)          (**r Absolute difference word *)
+  | Pabdl               (rd rs1 rs2: ireg)          (**r Absolute difference long *)
                         
   (** Arith RRI32 *)
   | Pcompiw (it: itest) (rd rs: ireg) (imm: int)    (**r comparison imm word *)
@@ -278,6 +281,7 @@ Inductive instruction : Type :=
   | Psrxil              (rd rs: ireg) (imm: int)    (**r shift right arithmetic imm word round to 0*)
   | Psrlil              (rd rs: ireg) (imm: int)    (**r shift right logical immediate long *)
   | Psrail              (rd rs: ireg) (imm: int)    (**r shift right arithmetic immediate long *)
+  | Pabdiw              (rd rs: ireg) (imm: int)    (**r Absolute difference word *)
 
   (** Arith RRI64 *)
   | Pcompil (it: itest) (rd rs: ireg) (imm: int64)  (**r comparison imm long *)
@@ -301,6 +305,7 @@ Inductive instruction : Type :=
   | Pcmoveuiw (bt: btest) (rcond rd : ireg) (imm: int) (** conditional move, unsigned semantics *) 
   | Pcmoveil (bt: btest) (rcond rd : ireg) (imm: int64) (** conditional move *) 
   | Pcmoveuil (bt: btest) (rcond rd : ireg) (imm: int64) (** conditional move, unsigned semantics *) 
+  | Pabdil               (rd rs : ireg) (imm: int64) (**r Absolute difference long *)
 .
 
 (** Correspondance between Asmblock and Asm *)
@@ -429,6 +434,9 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRR Asmvliw.Pfmaxd rd rs1 rs2      => Pfmaxd rd rs1 rs2
   | PArithRRR Asmvliw.Pfmaxw rd rs1 rs2      => Pfmaxw rd rs1 rs2
 
+  | PArithRRR Asmvliw.Pabdw rd rs1 rs2      => Pabdw rd rs1 rs2
+  | PArithRRR Asmvliw.Pabdl rd rs1 rs2      => Pabdl rd rs1 rs2
+
   (* RRI32 *)
   | PArithRRI32 (Asmvliw.Pcompiw it) rd rs imm => Pcompiw it rd rs imm
   | PArithRRI32 Asmvliw.Paddiw rd rs imm       => Paddiw rd rs imm
@@ -454,6 +462,8 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRI32 Asmvliw.Psrxil rd rs imm       => Psrxil rd rs imm
   | PArithRRI32 Asmvliw.Psrail rd rs imm       => Psrail rd rs imm
 
+  | PArithRRI32 Asmvliw.Pabdiw rd rs imm      => Pabdiw rd rs imm
+
   (* RRI64 *)
   | PArithRRI64 (Asmvliw.Pcompil it) rd rs imm => Pcompil it rd rs imm
   | PArithRRI64 Asmvliw.Paddil rd rs imm       => Paddil rd rs imm
@@ -470,6 +480,8 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRI64 Asmvliw.Pandnil rd rs imm      => Pandnil rd rs imm
   | PArithRRI64 Asmvliw.Pornil rd rs imm       => Pornil rd rs imm
 
+  | PArithRRI64 Asmvliw.Pabdil rd rs imm      => Pabdil rd rs imm
+
   (** ARRR *)
   | PArithARRR Asmvliw.Pmaddw rd rs1 rs2       => Pmaddw rd rs1 rs2
   | PArithARRR Asmvliw.Pmaddl rd rs1 rs2       => Pmaddl rd rs1 rs2
diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v
index ac0b359e..78a766ee 100644
--- a/kvx/Asmblockdeps.v
+++ b/kvx/Asmblockdeps.v
@@ -1613,6 +1613,8 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
   | Pfminw => "Pfminw"
   | Pfmaxd => "Pfmaxd"
   | Pfmaxw => "Pfmaxw"
+  | Pabdw => "Pabdw"
+  | Pabdl => "Pabdl"
   end.
 
 Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
@@ -1640,6 +1642,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
   | Psrlil => "Psrlil"
   | Psrail => "Psrail"
   | Psrxil => "Psrxil"
+  | Pabdiw => "Pabdiw"
   end.
 
 Definition string_of_name_rri64 (n: arith_name_rri64): pstring :=
@@ -1658,6 +1661,7 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring :=
   | Pnxoril => "Pnxoril"
   | Pandnil => "Pandnil"
   | Pornil => "Pornil"
+  | Pabdil => "Pabdil"
   end.
 
 Definition string_of_name_arrr (n: arith_name_arrr): pstring :=
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.
diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v
index 6d60445a..3fa184c6 100644
--- a/kvx/Asmvliw.v
+++ b/kvx/Asmvliw.v
@@ -475,6 +475,9 @@ Inductive arith_name_rrr : Type :=
   | Pfminw                                          (**r float min word *)
   | Pfmaxd                                          (**r float max double *)
   | Pfmaxw                                          (**r float max word *)
+
+  | Pabdw                          (**r absolute value of difference *)
+  | Pabdl                          (**r absolute value of difference *)
 .
 
 Inductive arith_name_rri32 : Type :=
@@ -502,6 +505,7 @@ Inductive arith_name_rri32 : Type :=
   | Psrlil                                          (**r shift right logical immediate long *)
   | Psrail                                          (**r shift right arithmetic immediate long *)
   | Psrxil                                          (**r shift right arithmetic immediate long round to 0*)
+  | Pabdiw                          (**r absolute value of difference *)
 .
 
 Inductive arith_name_rri64 : Type :=
@@ -519,6 +523,7 @@ Inductive arith_name_rri64 : Type :=
   | Pnxoril                                         (**r nxor immediate long *) 
   | Pandnil                                         (**r andn immediate long *)
   | Pornil                                          (**r orn immediate long *)
+  | Pabdil                          (**r absolute value of difference *)
 .
 
 Inductive arith_name_arrr : Type :=
@@ -1040,6 +1045,9 @@ Definition arith_eval_rrr n v1 v2 :=
 
   | Prevsubxw shift => ExtValues.revsubx (int_of_shift1_4 shift) v1 v2
   | Prevsubxl shift => ExtValues.revsubxl (int_of_shift1_4 shift) v1 v2
+
+  | Pabdw => ExtValues.absdiff v1 v2
+  | Pabdl => ExtValues.absdiffl v1 v2
   end.
 
 Definition arith_eval_rri32 n v i :=
@@ -1067,6 +1075,7 @@ Definition arith_eval_rri32 n v i :=
   | Psrail  => Val.shrl  v (Vint i)
   | Paddxiw shift => ExtValues.addx (int_of_shift1_4 shift) v (Vint i)
   | Prevsubxiw shift => ExtValues.revsubx (int_of_shift1_4 shift) v (Vint i)
+  | Pabdiw => ExtValues.absdiff v (Vint i)
   end.
 
 Definition arith_eval_rri64 n v i :=
@@ -1085,6 +1094,7 @@ Definition arith_eval_rri64 n v i :=
   | Pornil  => Val.orl (Val.notl v) (Vlong i)
   | Paddxil shift => ExtValues.addxl (int_of_shift1_4 shift) v (Vlong i)
   | Prevsubxil shift => ExtValues.revsubxl (int_of_shift1_4 shift) v (Vlong i)
+  | Pabdil => ExtValues.absdiffl v (Vlong i)
   end.
 
 Definition cmove bt v1 v2 v3 :=
diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v
index a0473d07..e3e4f95d 100644
--- a/kvx/Builtins1.v
+++ b/kvx/Builtins1.v
@@ -16,7 +16,7 @@
 (** Platform-specific built-in functions *)
 
 Require Import String Coqlib.
-Require Import AST Integers Floats Values ExtFloats.
+Require Import AST Integers Floats Values ExtFloats ExtValues.
 Require Import Builtins0.
 
 Inductive platform_builtin : Type :=
@@ -31,7 +31,9 @@ Inductive platform_builtin : Type :=
 | BI_fp_udiv32
 | BI_fp_udiv64
 | BI_fp_umod32
-| BI_fp_umod64.
+| BI_fp_umod64
+| BI_abs
+| BI_absl.
 
 Local Open Scope string_scope.
 
@@ -48,6 +50,8 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
   :: ("__builtin_fp_udiv64", BI_fp_udiv64)
   :: ("__builtin_fp_umod32", BI_fp_umod32)
   :: ("__builtin_fp_umod64", BI_fp_umod64)
+  :: ("__builtin_abs", BI_abs)
+  :: ("__builtin_absl", BI_absl)
   :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
@@ -70,6 +74,10 @@ Definition platform_builtin_sig (b: platform_builtin) : signature :=
       mksignature (Tint :: Tint :: nil) Tint cc_default
   | BI_fp_umod64 =>
       mksignature (Tlong :: Tlong :: nil) Tlong cc_default
+  | BI_abs =>
+      mksignature (Tint :: nil) Tint cc_default
+  | BI_absl =>
+      mksignature (Tlong :: nil) Tlong cc_default
   end.
 
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
@@ -98,4 +106,6 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl
        (fun n1 n2 => if Int64.eq n2 Int64.zero
                      then None
                      else Some (Int64.modu n1 n2))
+  | BI_abs => mkbuiltin_n1t Tint Tint ExtValues.int_abs
+  | BI_absl => mkbuiltin_n1t Tlong Tlong ExtValues.long_abs
   end.
diff --git a/kvx/CBuiltins.ml b/kvx/CBuiltins.ml
index 5ca5ddba..d712eecd 100644
--- a/kvx/CBuiltins.ml
+++ b/kvx/CBuiltins.ml
@@ -145,6 +145,10 @@ let builtins = {
     (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false);
     "__builtin_fp_umod64",
     (TInt(IULong, []), [TInt(IULong, []); TInt(IULong, [])], false);
+    "__builtin_abs",
+      (TInt(IInt, []), [TInt(IInt, [])], false);
+    "__builtin_absl",
+      (TInt(ILong, []), [TInt(ILong, [])], false);
 ]
 }
 
diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v
index c478f70b..f08c1157 100644
--- a/kvx/ExtValues.v
+++ b/kvx/ExtValues.v
@@ -21,14 +21,14 @@ Require Import Lia.
 
 Open Scope Z_scope.
 
-Definition abs_diff (x y : Z) := Z.abs (x - y).
-Definition abs_diff2 (x y : Z) :=
+Definition Z_abs_diff (x y : Z) := Z.abs (x - y).
+Definition Z_abs_diff2 (x y : Z) :=
   if x <=? y then y - x else x - y.
-Lemma abs_diff2_correct :
-  forall x y : Z, (abs_diff x y) = (abs_diff2 x y).
+Lemma Z_abs_diff2_correct :
+  forall x y : Z, (Z_abs_diff x y) = (Z_abs_diff2 x y).
 Proof.
   intros.
-  unfold abs_diff, abs_diff2.
+  unfold Z_abs_diff, Z_abs_diff2.
   unfold Z.leb.
   pose proof (Z.compare_spec x y) as Hspec.
   inv Hspec.
@@ -816,6 +816,98 @@ Definition my_div (a b : val) :=
   let x := fmaddf invb_d alpha invb_d in
   Val.mulf (Val.maketotal (Val.floatofintu a)) x.
 
-(*
-Compute (my_div (Vint (Int.repr 3)) (Vint (Int.repr 5))).
-*)
+Definition int_abs i1 := Int.repr (Z.abs (Int.signed i1)).
+Definition long_abs i1 := Int64.repr (Z.abs (Int64.signed i1)).
+
+Definition int_absdiff i1 i2 :=
+             Int.repr (Z_abs_diff (Int.signed i1) (Int.signed i2)).
+
+Definition long_absdiff i1 i2 :=
+             Int64.repr (Z_abs_diff (Int64.signed i1) (Int64.signed i2)).
+
+Lemma int_absdiff_zero :
+  forall i, int_abs i = int_absdiff i Int.zero.
+Proof.
+  intro. unfold int_abs, int_absdiff, Z_abs_diff.
+  change (Int.signed Int.zero) with 0%Z.
+  rewrite Z.sub_0_r.
+  reflexivity.
+Qed.
+
+Lemma long_absdiff_zero :
+  forall i, long_abs i = long_absdiff i Int64.zero.
+Proof.
+  intro. unfold long_abs, long_absdiff, Z_abs_diff.
+  change (Int64.signed Int64.zero) with 0%Z.
+  rewrite Z.sub_0_r.
+  reflexivity.
+Qed.
+
+Definition double_op_int f v1 v2 :=
+  match v1, v2 with
+  | (Vint i1), (Vint i2) => Vint (f i1 i2)
+  |  _, _ => Vundef
+  end.
+
+Definition double_op_long f v1 v2 :=
+  match v1, v2 with
+  | (Vlong i1), (Vlong i2) => Vlong (f i1 i2)
+  | _, _ => Vundef
+  end.
+
+Definition absdiff := double_op_int int_absdiff.
+Definition absdiffl := double_op_long long_absdiff.
+
+Definition abs v1 :=
+  match v1 with
+  | Vint x => Vint (Int.repr (Z.abs (Int.signed x)))
+  | _ => Vundef
+  end.
+
+Definition absl v1 :=
+  match v1 with
+  | Vlong x => Vlong (Int64.repr (Z.abs (Int64.signed x)))
+  | _ => Vundef
+  end.
+
+Lemma absdiff_zero_correct:
+  forall v, abs v = absdiff v (Vint Int.zero).
+Proof.
+  intro. destruct v; cbn; try reflexivity.
+  f_equal. unfold int_absdiff, Z_abs_diff.
+  change (Int.unsigned Int.zero) with 0%Z.
+  rewrite Z.sub_0_r.
+  reflexivity.
+Qed.
+
+Lemma absdiffl_zero_correct:
+  forall v, absl v = absdiffl v (Vlong Int64.zero).
+Proof.
+  intro. destruct v; cbn; try reflexivity.
+  f_equal. unfold long_absdiff, Z_abs_diff.
+  change (Int64.unsigned Int64.zero) with 0%Z.
+  rewrite Z.sub_0_r.
+  reflexivity.
+Qed.
+
+Remark absdiff_inject:
+  forall f v1 v1' v2 v2'
+  (INJ1 : Val.inject f v1 v1')
+  (INJ2 : Val.inject f v2 v2'),
+  Val.inject f (absdiff v1 v2) (absdiff v1' v2').
+Proof.
+  intros.
+  inv INJ1; cbn; try constructor.
+  inv INJ2; cbn; constructor.
+Qed.
+
+Remark absdiffl_inject:
+  forall f v1 v1' v2 v2'
+  (INJ1 : Val.inject f v1 v1')
+  (INJ2 : Val.inject f v2 v2'),
+  Val.inject f (absdiffl v1 v2) (absdiffl v1' v2').
+Proof.
+  intros.
+  inv INJ1; cbn; try constructor.
+  inv INJ2; cbn; constructor.
+Qed.
diff --git a/kvx/FPExtra.v b/kvx/FPExtra.v
index 05fd8842..9e3b55b6 100644
--- a/kvx/FPExtra.v
+++ b/kvx/FPExtra.v
@@ -15,9 +15,11 @@ Definition e_addl a b := Eop Oaddl (a ::: b ::: Enil).
 Definition e_orl  a b := Eop Oorl  (a ::: b ::: Enil).
 Definition e_constl n := Eop (Olongconst (Int64.repr n)) Enil.
 Definition e_float_of_longu a  := Eop Ofloatoflongu (a ::: Enil).
+Definition e_float_of_long a  := Eop Ofloatoflong (a ::: Enil).
 Definition e_single_of_float a := Eop Osingleoffloat (a ::: Enil).
 Definition e_ite ty c vc v1 v2 := Eop (Osel c ty) (v1 ::: v2 ::: vc ::: Enil).
 Definition e_cmpluimm c v n := Eop (Ocmp (Ccompluimm c n)) (v ::: Enil).
+Definition e_absl a := Eop (Oabsdifflimm Int64.zero) (a ::: Enil).
 
 Definition a_var := Eletvar 0%nat.
 
@@ -58,3 +60,58 @@ Proof.
   lia.
 Qed.
 
+Definition e_single_of_long a :=
+  Elet a (e_single_of_float (e_float_of_long
+    (e_ite Tlong (Ccompu0 Cne) (e_cmpluimm Cle (e_absl a_var) (Int64.repr (2^53))) a_var
+           (e_andl (e_orl a_var (e_addl (e_andl a_var (e_constl 2047))
+                                        (e_constl 2047)))
+                   (e_constl (-2048))))))%Z.
+
+Theorem e_single_of_long_correct :
+  forall (ge : genv)  (sp: val) cmenv memenv
+         (le : letenv) (expr_a : expr) (va : val)
+         (EVAL_a : eval_expr ge sp cmenv memenv le expr_a va),
+  eval_expr ge sp cmenv memenv le (e_single_of_long expr_a)
+            (Val.maketotal (Val.singleoflong va)).
+Proof.
+  intros.
+  unfold e_single_of_long.
+  repeat econstructor. eassumption.
+  cbn.
+  destruct va; cbn.
+  all: try reflexivity.
+  f_equal.
+  unfold Int64.ltu.
+  change (Int64.unsigned (Int64.repr 9007199254740992))%Z with 9007199254740992%Z.
+  destruct zlt as [LT | GE]; cbn.
+  { change (Int.eq Int.zero Int.zero) with true. cbn.
+    f_equal.
+    symmetry.
+    apply Float32.of_long_double_2.
+    unfold long_absdiff, Z_abs_diff in LT.
+    change (Int64.signed Int64.zero) with 0%Z in LT.
+    rewrite Z.sub_0_r in LT.
+    rewrite Int64.unsigned_repr in LT.
+    lia.
+    pose proof (Int64.signed_range i).
+    change Int64.min_signed with (-9223372036854775808)%Z in *.
+    change Int64.max_signed with (9223372036854775807)%Z in *.
+    change Int64.max_unsigned with (18446744073709551615)%Z.
+    lia.
+  }
+  change (Int.eq Int.one Int.zero) with false. cbn.
+  f_equal.
+  symmetry.
+  apply Float32.of_long_double_1.
+  unfold long_absdiff, Z_abs_diff in GE.
+  change (Int64.signed Int64.zero) with 0%Z in GE.
+  rewrite Z.sub_0_r in GE.
+  rewrite Int64.unsigned_repr in GE.
+  lia.
+  pose proof (Int64.signed_range i).
+  change Int64.min_signed with (-9223372036854775808)%Z in *.
+  change Int64.max_signed with (9223372036854775807)%Z in *.
+  change Int64.max_unsigned with (18446744073709551615)%Z.
+  lia.
+Qed.
+
diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v
index 455af70e..5a3b7190 100644
--- a/kvx/NeedOp.v
+++ b/kvx/NeedOp.v
@@ -139,6 +139,10 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Osel c ty => nv :: nv :: needs_of_condition0 c
   | Oselimm c imm
   | Osellimm c imm => nv :: needs_of_condition0 c
+  | Oabsdiff => op2 (default nv)
+  | Oabsdiffimm _ => op1 (default nv)
+  | Oabsdiffl => op2 (default nv)
+  | Oabsdifflimm _ => op1 (default nv)
   end.
 
 Definition operation_is_redundant (op: operation) (nv: nval): bool :=
diff --git a/kvx/Op.v b/kvx/Op.v
index 8549fc38..d726afde 100644
--- a/kvx/Op.v
+++ b/kvx/Op.v
@@ -224,7 +224,11 @@ Inductive operation : Type :=
   | Oinsfl (stop : Z) (start : Z)
   | Osel (c0 : condition0) (ty : typ)
   | Oselimm (c0 : condition0) (imm: int)
-  | Osellimm (c0 : condition0) (imm: int64).
+  | Osellimm (c0 : condition0) (imm: int64)
+  | Oabsdiff
+  | Oabsdiffimm (imm: int)
+  | Oabsdiffl
+  | Oabsdifflimm (imm: int64).
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -486,6 +490,10 @@ Definition eval_operation
   | Osel c ty, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 v2 ty)
   | Oselimm c imm, v1::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vint imm) Tint)
   | Osellimm c imm, v1::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vlong imm) Tlong)
+  | Oabsdiff, v0::v1::nil => Some(ExtValues.absdiff v0 v1)
+  | (Oabsdiffimm n1), v0::nil => Some(ExtValues.absdiff v0 (Vint n1))
+  | Oabsdiffl, v0::v1::nil => Some(ExtValues.absdiffl v0 v1)
+  | (Oabsdifflimm n1), v0::nil => Some(ExtValues.absdiffl v0 (Vlong n1))
   | _, _ => None
   end.
 
@@ -707,6 +715,10 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osel c ty => (ty :: ty :: arg_type_of_condition0 c :: nil, ty)
   | Oselimm c ty => (Tint :: arg_type_of_condition0 c :: nil, Tint)
   | Osellimm c ty => (Tlong :: arg_type_of_condition0 c :: nil, Tlong)
+  | Oabsdiff => (Tint :: Tint :: nil, Tint)
+  | Oabsdiffimm _ => (Tint :: nil, Tint)
+  | Oabsdiffl => (Tlong :: Tlong :: nil, Tlong)
+  | Oabsdifflimm _ => (Tlong :: nil, Tlong)
   end.
 
 (* FIXME: two Tptr ?! *)
@@ -1048,6 +1060,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - unfold Val.select. destruct (eval_condition0 _ _ m).
     + apply Val.normalize_type.
     + constructor.
+  (* oabsdiff *)
+  - destruct v0; destruct v1; cbn; trivial.
+  - destruct v0; cbn; trivial.
+  - destruct v0; destruct v1; cbn; trivial.
+  - destruct v0; cbn; trivial.
 Qed.
 
 Definition is_trapping_op (op : operation) :=
@@ -1768,6 +1785,11 @@ Proof.
       symmetry.
       eapply eval_condition0_inj; eassumption.
     + left. trivial.
+  (* Oabsdiff *)
+  - apply ExtValues.absdiff_inject; trivial.   
+  - apply ExtValues.absdiff_inject; trivial.   
+  - apply ExtValues.absdiffl_inject; trivial.   
+  - apply ExtValues.absdiffl_inject; trivial.   
 Qed.
 
 Lemma eval_addressing_inj:
diff --git a/kvx/PostpassSchedulingOracle.ml b/kvx/PostpassSchedulingOracle.ml
index e752624c..c729c72d 100644
--- a/kvx/PostpassSchedulingOracle.ml
+++ b/kvx/PostpassSchedulingOracle.ml
@@ -34,6 +34,7 @@ type real_instruction =
   | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sbfxw | Sraw | Srlw | Sllw | Srsw | Rorw | Xorw
   | Addd | Andd | Compd | Muld | Ord | Sbfd | Sbfxd | Srad | Srld | Slld | Srsd | Xord
   | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd
+  | Abdw  | Abdd
   | Maddw | Maddd | Msbfw | Msbfd | Cmoved
   | Make | Nop | Extfz | Extfs | Insf
   | Addxw | Addxd
@@ -90,7 +91,7 @@ let arith_rr_real = function
   | Pfixedwrzz | Pfixedwrne ->       Fixedw
   | Pfixeduwrzz | Pfixeduwrne ->      Fixeduw
   | Pfixeddrzz | Pfixeddrne -> Fixedd
-  | Pfixedudrzz| Pfixedudrne -> Fixedud
+  | Pfixedudrzz | Pfixedudrne -> Fixedud
   | Pfixeddrzz_i32 ->   Fixedd
   | Pfixedudrzz_i32 ->  Fixedud
 
@@ -143,6 +144,8 @@ let arith_rrr_real = function
   | Pfminw ->         Fminw
   | Pfmaxd ->         Fmaxd
   | Pfmaxw ->         Fmaxw
+  | Pabdw ->          Abdw
+  | Pabdl ->          Abdd
 
 let arith_rri32_real = function
   | Pcompiw it ->   Compw
@@ -168,6 +171,7 @@ let arith_rri32_real = function
   | Psrlil ->       Srld
   | Psrail ->       Srad
   | Psrxil ->       Srsd
+  | Pabdiw ->       Abdw
 
 let arith_rri64_real = function
   | Pcompil it ->   Compd
@@ -184,6 +188,7 @@ let arith_rri64_real = function
   | Pnxoril ->      Nxord
   | Pandnil ->      Andnd
   | Pornil ->       Ornd
+  | Pabdil ->       Abdd
 
 
 let arith_arr_real = function
@@ -603,11 +608,11 @@ let rec_to_usage r =
       (match encoding with None | Some U6 | Some S10 -> alu_lite
                           | Some U27L5 | Some U27L10 -> alu_lite_x
                           | Some E27U27L10 -> alu_lite_y)
-  | Addxw -> 
+  | Addxw | Abdw -> 
       (match encoding with None | Some U6 | Some S10 -> alu_lite 
                           | Some U27L5 | Some U27L10 -> alu_lite_x
                           | _ -> raise InvalidEncoding)
-  | Addxd -> 
+  | Addxd | Abdd -> 
       (match encoding with None | Some U6 | Some S10 -> alu_lite 
                           | Some U27L5 | Some U27L10 -> alu_lite_x
                           | Some E27U27L10 -> alu_lite_y)
@@ -681,6 +686,7 @@ let real_inst_to_latency = function
   | Addd | Andd | Compd | Ord | Sbfd | Sbfxd | Srad | Srsd | Srld | Slld | Xord | Make
   | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved | Addxw | Addxd
   | Fmind | Fmaxd | Fminw | Fmaxw
+  | Abdw | Abdd
         -> 1
   | Floatwz | Floatuwz | Fixeduw | Fixedw | Floatdz | Floatudz | Fixedd | Fixedud -> 4
   | Mulw | Muld | Maddw | Maddd | Msbfw | Msbfd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
diff --git a/kvx/SelectLong.vp b/kvx/SelectLong.vp
index 3598025a..9df3212b 100644
--- a/kvx/SelectLong.vp
+++ b/kvx/SelectLong.vp
@@ -452,7 +452,10 @@ Definition longuofsingle (e: expr) := longuoffloat (floatofsingle e).
 Definition use_inlined_fp_conversions := true.
 Opaque use_inlined_fp_conversions.
 
-Definition singleoflong (e: expr) := SplitLong.singleoflong e.
+Definition singleoflong (e: expr) :=
+  if use_inlined_fp_conversions
+  then FPExtra.e_single_of_long e
+  else SplitLong.singleoflong e.
 
 Definition singleoflongu (e: expr) :=
   if use_inlined_fp_conversions
diff --git a/kvx/SelectLongproof.v b/kvx/SelectLongproof.v
index b858158b..ca32d69a 100644
--- a/kvx/SelectLongproof.v
+++ b/kvx/SelectLongproof.v
@@ -933,7 +933,10 @@ Qed.
 Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong.
 Proof.
   unfold singleoflong; red; intros.
-  eapply SplitLongproof.eval_singleoflong; eauto.
+  destruct use_inlined_fp_conversions.
+  - econstructor. split. apply FPExtra.e_single_of_long_correct.
+    eassumption. rewrite H0. cbn. constructor.
+  - eapply SplitLongproof.eval_singleoflong; eauto.
 Qed.
 
 Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu.
diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp
index 089afe1d..63c7d73b 100644
--- a/kvx/SelectOp.vp
+++ b/kvx/SelectOp.vp
@@ -742,6 +742,24 @@ Nondetfunction gen_fmaf args :=
   | _ => None
   end.
 
+Definition select_abs (e1 : expr) :=
+  Eop (Oabsdiffimm Int.zero) (e1 ::: Enil).
+
+Definition select_absl (e1 : expr) :=
+  Eop (Oabsdifflimm Int64.zero) (e1 ::: Enil).
+  
+Definition gen_abs args :=
+  match args with
+  | e1:::Enil => Some (select_abs e1)
+  | _ => None
+  end.
+
+Definition gen_absl args :=
+  match args with
+  | e1:::Enil => Some (select_absl e1)
+  | _ => None
+  end.
+
 Require FPDivision32 FPDivision64.
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
@@ -770,6 +788,8 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
                      | a:::b:::Enil => Some (FPDivision64.fp_modu64 a b)
                      | _ => None
                      end)
+  | BI_abs => gen_abs args
+  | BI_absl => gen_absl args
   end.
 End SELECT.
 
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index cffa2583..a45d367f 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1883,6 +1883,57 @@ Proof.
       destruct v2; simpl; trivial.
 Qed.
 
+Lemma eval_abs:
+  forall al a vl v le,
+  gen_abs al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem BI_abs vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  unfold gen_abs.
+  intros until le.
+  intros SELECT Heval BUILTIN.
+  inv Heval. discriminate.
+  inv H0. 2: discriminate.
+  cbn in BUILTIN.
+  inv BUILTIN.
+  inv SELECT.
+  econstructor; split.
+  { repeat (econstructor + eassumption).
+  }
+  destruct v1; try constructor.
+  cbn.
+  unfold int_abs, int_absdiff, Z_abs_diff.
+  change (Int.signed Int.zero) with 0%Z.
+  rewrite Z.sub_0_r.
+  constructor.
+Qed.
+
+Lemma eval_absl:
+  forall al a vl v le,
+  gen_absl al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem BI_absl vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  unfold gen_abs.
+  intros until le.
+  intros SELECT Heval BUILTIN.
+  inv Heval. discriminate.
+  inv H0. 2: discriminate.
+  cbn in BUILTIN.
+  inv BUILTIN.
+  inv SELECT.
+  econstructor; split.
+  { repeat (econstructor + eassumption).
+  }
+  destruct v1; try constructor.
+  cbn.
+  unfold long_abs, long_absdiff, Z_abs_diff.
+  change (Int64.signed Int64.zero) with 0%Z.
+  rewrite Z.sub_0_r.
+  constructor.
+Qed.
 
 Require FPDivision32.
 
@@ -1995,6 +2046,7 @@ Proof.
     }
     inv EVAL.
     constructor.
+  - apply eval_abs; assumption.
+  - apply eval_absl; assumption.
 Qed.
-
 End CMCONSTR.
diff --git a/kvx/TargetPrinter.ml b/kvx/TargetPrinter.ml
index 01733858..88143bfa 100644
--- a/kvx/TargetPrinter.ml
+++ b/kvx/TargetPrinter.ml
@@ -739,6 +739,12 @@ module Target (*: TARGET*) =
       | Pfinvw (rd, rs1) ->
          fprintf oc "	finvw	%a = %a\n" ireg rd ireg rs1
 
+      | Pabdw (rd, rs1, rs2) ->
+         fprintf oc "	abdw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Pabdl (rd, rs1, rs2) ->
+         fprintf oc "	abdd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         
+
       (* Arith RRI32 instructions *)
       | Pcompiw (it, rd, rs, imm) ->
          fprintf oc "	compw.%a	%a = %a, %a\n" icond it ireg rd ireg rs coqint imm
@@ -770,6 +776,8 @@ module Target (*: TARGET*) =
          fprintf oc "	andnw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Porniw (rd, rs, imm) -> 
          fprintf oc "	ornw	%a = %a, %a\n" ireg rd ireg rs coqint imm
+      | Pabdiw (rd, rs, imm) -> 
+         fprintf oc "	abdw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Psraiw (rd, rs, imm) ->
          fprintf oc "	sraw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Psrxiw (rd, rs, imm) ->
@@ -823,6 +831,8 @@ module Target (*: TARGET*) =
          fprintf oc "	andnd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Pornil (rd, rs, imm) -> 
          fprintf oc "	ornd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+      | Pabdil (rd, rs, imm) -> 
+         fprintf oc "	abdd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Pmaddil (rd, rs, imm) ->
          fprintf oc "	maddd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
 
diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v
index 4909a25b..52658b43 100644
--- a/kvx/ValueAOp.v
+++ b/kvx/ValueAOp.v
@@ -156,6 +156,12 @@ Definition eval_static_insfl stop start prev fld :=
     end
   else Vtop.
 
+Definition absdiff := binop_int
+   (fun i1 i2 => ExtValues.int_absdiff i1 i2).
+
+Definition absdiffl := binop_long
+   (fun i1 i2 => ExtValues.long_absdiff i1 i2).
+              
 Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with
   | Omove, v1::nil => v1
@@ -312,6 +318,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Osel c ty, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 v2
   | Oselimm c imm, v1::vc::nil => select (eval_static_condition0 c vc) v1 (I imm)
   | Osellimm c imm, v1::vc::nil => select (eval_static_condition0 c vc) v1 (L imm)
+  | Oabsdiff, v1::v2::nil => absdiff v1 v2
+  | (Oabsdiffimm n2), v1::nil => absdiff v1 (I n2)
+  | Oabsdiffl, v1::v2::nil => absdiffl v1 v2
+  | (Oabsdifflimm n2), v1::nil => absdiffl v1 (L n2)
   | _, _ => Vbot
   end.
 
@@ -323,6 +333,26 @@ Hypothesis GENV: genv_match bc ge.
 Variable sp: block.
 Hypothesis STACK: bc sp = BCstack.
 
+Lemma absdiff_sound:
+  forall v x w y
+         (vMATCH : vmatch bc v x)
+         (wMATCH : vmatch bc w y),
+    vmatch bc (ExtValues.absdiff v w) (absdiff x y).
+Proof.
+  intros.
+  apply binop_int_sound; trivial.
+Qed.
+
+Lemma absdiffl_sound:
+  forall v x w y
+         (vMATCH : vmatch bc v x)
+         (wMATCH : vmatch bc w y),
+    vmatch bc (ExtValues.absdiffl v w) (absdiffl x y).
+Proof.
+  intros.
+  apply binop_long_sound; trivial.
+Qed.
+
 Lemma minf_sound:
   forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y).
 Proof.
@@ -597,6 +627,11 @@ Proof.
   - apply select_sound; auto with va. eapply eval_static_condition0_sound; eauto.
     (* select long imm *)
   - apply select_sound; auto with va. eapply eval_static_condition0_sound; eauto.
+    (* Oabsdiff *)
+  - apply absdiff_sound; auto with va.
+  - apply absdiff_sound; auto with va.
+  - apply absdiffl_sound; auto with va.
+  - apply absdiffl_sound; auto with va.
 Qed.
 
 End SOUNDNESS.