Merge remote-tracking branch 'origin/kvx-work' into merge_absint

20 files changed, 476 insertions, 47 deletions

diff --git a/configure b/configure
index 61a6697c..685ce390 100755
--- a/configure
+++ b/configure
@@ -821,6 +821,7 @@ CFLAGS= -D __KVX_COS__
 SIMU=kvx-cluster -- 
 BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
     Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\
+    FPExtra.v \\
     ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
     Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\
     AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v
diff --git a/kvx/Archi.v b/kvx/Archi.v
index 6d59a3d1..b1739421 100644
--- a/kvx/Archi.v
+++ b/kvx/Archi.v
@@ -16,7 +16,7 @@
 (** Architecture-dependent parameters for MPPA KVX. Mostly copied from the Risc-V backend *)
 
 Require Import ZArith List.
-Require Import Binary Bits.
+From Flocq Require Import Binary Bits.
 
 Definition ptr64 := true.
 
diff --git a/kvx/Asm.v b/kvx/Asm.v
index fd20316c..c8303d37 100644
--- a/kvx/Asm.v
+++ b/kvx/Asm.v
@@ -243,6 +243,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 *)
@@ -270,6 +273,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 *)
@@ -293,6 +297,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 *)
@@ -417,6 +422,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
@@ -442,6 +450,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
@@ -458,6 +468,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 a9786e0a..b1895ee6 100644
--- a/kvx/Asmblockdeps.v
+++ b/kvx/Asmblockdeps.v
@@ -1609,6 +1609,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 :=
@@ -1636,6 +1638,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 :=
@@ -1654,6 +1657,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 ab827b1c..fd41dfdd 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)
@@ -889,7 +901,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 45b230e6..0ce2ed69 100644
--- a/kvx/Asmvliw.v
+++ b/kvx/Asmvliw.v
@@ -472,6 +472,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 :=
@@ -499,6 +502,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 :=
@@ -516,6 +520,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 :=
@@ -1033,6 +1038,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 :=
@@ -1060,6 +1068,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 :=
@@ -1078,6 +1087,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 441345bf..b5fc7459 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 :=
@@ -25,7 +25,9 @@ Inductive platform_builtin : Type :=
 | BI_fminf
 | BI_fmaxf
 | BI_fma
-| BI_fmaf.
+| BI_fmaf
+| BI_abs
+| BI_absl.
 
 Local Open Scope string_scope.
 
@@ -36,6 +38,8 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
   :: ("__builtin_fmaxf", BI_fmaxf)
   :: ("__builtin_fma", BI_fma)
   :: ("__builtin_fmaf", BI_fmaf)
+  :: ("__builtin_abs", BI_abs)
+  :: ("__builtin_absl", BI_absl)
   :: nil.
 
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
@@ -48,6 +52,10 @@ Definition platform_builtin_sig (b: platform_builtin) : signature :=
       mksignature (Tfloat :: Tfloat :: Tfloat :: nil) Tfloat cc_default
   | BI_fmaf =>
       mksignature (Tsingle :: Tsingle :: Tsingle :: nil) Tsingle 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)) :=
@@ -58,4 +66,6 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl
   | BI_fmaxf => mkbuiltin_n2t Tsingle Tsingle Tsingle ExtFloat32.max
   | BI_fma => mkbuiltin_n3t Tfloat Tfloat Tfloat Tfloat Float.fma
   | BI_fmaf => mkbuiltin_n3t Tsingle Tsingle Tsingle Tsingle Float32.fma
+  | 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 7398e0f4..4d016453 100644
--- a/kvx/CBuiltins.ml
+++ b/kvx/CBuiltins.ml
@@ -133,6 +133,10 @@ let builtins = {
     "__builtin_fmaf",
       (TFloat(FFloat, []),
        [TFloat(FFloat, []); TFloat(FFloat, []); TFloat(FFloat, [])], 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 b4e14898..c493f708 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.
@@ -754,3 +754,99 @@ Definition fmaddfs := triple_op_single (fun f1 f2 f3 => Float32.fma f2 f3 f1).
 
 Definition fmsubf := triple_op_float (fun f1 f2 f3 => Float.fma (Float.neg f2) f3 f1).
 Definition fmsubfs := triple_op_single (fun f1 f2 f3 => Float32.fma (Float32.neg f2) f3 f1).
+
+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
new file mode 100644
index 00000000..9e3b55b6
--- /dev/null
+++ b/kvx/FPExtra.v
@@ -0,0 +1,117 @@
+Require Import Coqlib.
+Require Import Compopts.
+Require Import AST Integers Floats.
+Require Import Op CminorSel.
+Require Import OpHelpers.
+Require Import SelectOp SplitLong.
+Require Import Values ExtValues.
+Require Import DecBoolOps.
+
+Local Open Scope cminorsel_scope.
+Local Open Scope string_scope.
+
+Definition e_andl a b := Eop Oandl (a ::: b ::: Enil).
+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.
+
+Definition e_single_of_longu a :=
+  Elet a (e_single_of_float (e_float_of_longu
+    (e_ite Tlong (Ccompu0 Cne) (e_cmpluimm Cle 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_longu_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_longu expr_a)
+            (Val.maketotal (Val.singleoflongu va)).
+Proof.
+  intros.
+  unfold e_single_of_longu.
+  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_longu_double_2.
+    lia.
+  }
+  change (Int.eq Int.one Int.zero) with false. cbn.
+  f_equal.
+  symmetry.
+  apply Float32.of_longu_double_1.
+  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 4578b4e8..cc86fc88 100644
--- a/kvx/NeedOp.v
+++ b/kvx/NeedOp.v
@@ -137,6 +137,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 4458adb3..86db0c0a 100644
--- a/kvx/Op.v
+++ b/kvx/Op.v
@@ -219,7 +219,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. *)
@@ -476,6 +480,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.
 
@@ -691,6 +699,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 ?! *)
@@ -1026,6 +1038,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) :=
@@ -1738,6 +1755,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 3f4520a6..3eb0b95f 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
@@ -47,7 +48,8 @@ type real_instruction =
   | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw
   | Fmind | Fminw | Fmaxd | Fmaxw | Finvw
   | Ffmaw | Ffmad | Ffmsw | Ffmsd
-  | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz | Fixedwz | Fixeduwz | Fixeddz | Fixedudz
+  | Fnarrowdw | Fwidenlwd | Floatwz | Floatuwz | Floatdz | Floatudz
+  | Fixedw | Fixeduw | Fixedd | Fixedud
   | Fcompw | Fcompd
 
 type ab_inst_rec = {
@@ -86,12 +88,12 @@ let arith_rr_real = function
   | Pfloatuwrnsz ->     Floatuwz
   | Pfloatudrnsz ->     Floatudz
   | Pfloatdrnsz ->      Floatdz
-  | Pfixedwrzz ->       Fixedwz
-  | Pfixeduwrzz ->      Fixeduwz
-  | Pfixeddrzz ->       Fixeddz
-  | Pfixedudrzz ->      Fixedudz
-  | Pfixeddrzz_i32 ->   Fixeddz
-  | Pfixedudrzz_i32 ->  Fixedudz
+  | Pfixedwrzz  ->       Fixedw
+  | Pfixeduwrzz ->      Fixeduw
+  | Pfixeddrzz -> Fixedd
+  | Pfixedudrzz -> Fixedud
+  | Pfixeddrzz_i32 ->   Fixedd
+  | Pfixedudrzz_i32 ->  Fixedud
 
 let arith_rrr_real = function
   | Pcompw it ->      Compw
@@ -142,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
@@ -167,6 +171,7 @@ let arith_rri32_real = function
   | Psrlil ->       Srld
   | Psrail ->       Srad
   | Psrxil ->       Srsd
+  | Pabdiw ->       Abdw
 
 let arith_rri64_real = function
   | Pcompil it ->   Compd
@@ -183,6 +188,7 @@ let arith_rri64_real = function
   | Pnxoril ->      Nxord
   | Pandnil ->      Andnd
   | Pornil ->       Ornd
+  | Pabdil ->       Abdd
 
 
 let arith_arr_real = function
@@ -602,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)
@@ -643,7 +649,7 @@ let rec_to_usage r =
   (* TODO: check *)
   | Srsw | Srsd | Rorw -> (match encoding with None | Some U6 -> alu_lite | _ -> raise InvalidEncoding)
   | Extfz | Extfs | Insf -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding)
-  | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau
+  | Fixeduw | Fixedw | Floatwz | Floatuwz | Fixedd | Fixedud | Floatdz | Floatudz -> mau
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> 
       (match encoding with None | Some U6 | Some S10 -> lsu_auxw
                           | Some U27L5 | Some U27L10 -> lsu_auxw_x
@@ -656,8 +662,8 @@ let rec_to_usage r =
   | Get -> bcu_tiny_tiny_mau_xnop
   | Fnegd | Fnegw | Fabsd | Fabsw | Fwidenlwd
   | Fmind | Fmaxd | Fminw | Fmaxw -> alu_lite
-  | Fnarrowdw -> alu_full
-  | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw | Finvw
+  | Finvw | Fnarrowdw -> alu_full
+  | Faddd | Faddw | Fsbfd | Fsbfw | Fmuld | Fmulw
   | Ffmad | Ffmaw | Ffmsd | Ffmsw -> mau
 
 
@@ -680,8 +686,9 @@ 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 | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4
+  | 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 *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> 3
   | Sb | Sh | Sw | Sd | Sq | So -> 1 (* See kvx-Optimization.pdf page 19 *)
diff --git a/kvx/SelectLong.vp b/kvx/SelectLong.vp
index b3638eca..9df3212b 100644
--- a/kvx/SelectLong.vp
+++ b/kvx/SelectLong.vp
@@ -23,6 +23,7 @@ Require Import OpHelpers.
 Require Import SelectOp SplitLong.
 Require Import ExtValues.
 Require Import DecBoolOps.
+Require FPExtra.
 
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
@@ -433,28 +434,33 @@ Definition cmpl (c: comparison) (e1 e2: expr) :=
 (** ** Floating-point conversions *)
 
 Definition longoffloat (e: expr) :=
-  if Archi.splitlong then SplitLong.longoffloat e else 
   Eop Olongoffloat (e:::Enil).
 
 Definition longuoffloat (e: expr) :=
-  if Archi.splitlong then SplitLong.longuoffloat e else 
   Eop Olonguoffloat (e:::Enil).
 
 Definition floatoflong (e: expr) := 
-  if Archi.splitlong then SplitLong.floatoflong e else 
   Eop Ofloatoflong (e:::Enil).
 
 Definition floatoflongu (e: expr) := 
-  if Archi.splitlong then SplitLong.floatoflongu e else 
   Eop Ofloatoflongu (e:::Enil).
 
 Definition longofsingle (e: expr) := longoffloat (floatofsingle e).
 
 Definition longuofsingle (e: expr) := longuoffloat (floatofsingle e).
 
-Definition singleoflong (e: expr) := SplitLong.singleoflong e.
+Definition use_inlined_fp_conversions := true.
+Opaque use_inlined_fp_conversions.
 
-Definition singleoflongu (e: expr) := SplitLong.singleoflongu 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
+  then FPExtra.e_single_of_longu e
+  else SplitLong.singleoflongu e.
 
 End SELECT.
 
diff --git a/kvx/SelectLongproof.v b/kvx/SelectLongproof.v
index c3abdbc7..ca32d69a 100644
--- a/kvx/SelectLongproof.v
+++ b/kvx/SelectLongproof.v
@@ -884,32 +884,28 @@ Qed.
 
 Theorem eval_longoffloat: partial_unary_constructor_sound longoffloat Val.longoffloat.
 Proof.
-  unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL.
-  eapply SplitLongproof.eval_longoffloat; eauto.
+  unfold longoffloat; red; intros.
   TrivialExists.
   simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_longuoffloat: partial_unary_constructor_sound longuoffloat Val.longuoffloat.
 Proof.
-  unfold longuoffloat; red; intros. destruct Archi.splitlong eqn:SL.
-  eapply SplitLongproof.eval_longuoffloat; eauto.
+  unfold longuoffloat; red; intros.
   TrivialExists.
   simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong.
 Proof.
-  unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL.
-  eapply SplitLongproof.eval_floatoflong; eauto.
+  unfold floatoflong; red; intros.
   TrivialExists.
   simpl. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_floatoflongu: partial_unary_constructor_sound floatoflongu Val.floatoflongu.
 Proof.
-  unfold floatoflongu; red; intros. destruct Archi.splitlong eqn:SL.
-  eapply SplitLongproof.eval_floatoflongu; eauto.
+  unfold floatoflongu; red; intros.
   TrivialExists.
   simpl. rewrite H0. reflexivity.
 Qed.
@@ -936,16 +932,20 @@ Qed.
 
 Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong.
 Proof.
-  unfold singleoflong; red; intros. (* destruct Archi.splitlong eqn:SL. *)
-  eapply SplitLongproof.eval_singleoflong; eauto.
-(*   TrivialExists. *)
+  unfold singleoflong; red; intros.
+  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.
 Proof.
-  unfold singleoflongu; red; intros. (* destruct Archi.splitlong eqn:SL. *)
-  eapply SplitLongproof.eval_singleoflongu; eauto.
-(*   TrivialExists. *)
+  unfold singleoflongu; red; intros.
+  destruct use_inlined_fp_conversions.
+  - econstructor. split. apply FPExtra.e_single_of_longu_correct.
+    eassumption. rewrite H0. cbn. constructor.
+  - eapply SplitLongproof.eval_singleoflongu; eauto.
 Qed.
 
 End CMCONSTR.
diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp
index 4e1087f9..f243089d 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.
+
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
   match b with
   | BI_fmin => Some (Eop Ominf args)
@@ -750,6 +768,8 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr
   | BI_fmaxf => Some (Eop Omaxfs args)
   | BI_fma => gen_fma args
   | BI_fmaf => gen_fmaf args
+  | BI_abs => gen_abs args
+  | BI_absl => gen_absl args
   end.
 End SELECT.
 
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v
index 0ede1e2d..4ddf6ece 100644
--- a/kvx/SelectOpproof.v
+++ b/kvx/SelectOpproof.v
@@ -1883,6 +1883,58 @@ 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.
+
 Theorem eval_platform_builtin:
   forall bf al a vl v le,
   platform_builtin bf al = Some a ->
@@ -1896,6 +1948,7 @@ Proof.
        repeat (try econstructor; try eassumption)).
   - apply eval_fma; assumption.
   - apply eval_fmaf; assumption.
+  - apply eval_abs; assumption.
+  - apply eval_absl; assumption.
 Qed.
-
 End CMCONSTR.
diff --git a/kvx/TargetPrinter.ml b/kvx/TargetPrinter.ml
index 9e2e3776..8a311dbb 100644
--- a/kvx/TargetPrinter.ml
+++ b/kvx/TargetPrinter.ml
@@ -731,6 +731,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
@@ -762,6 +768,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) ->
@@ -815,6 +823,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 87554258..ddfe94f3 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
@@ -308,6 +314,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.
 
@@ -319,6 +329,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.
@@ -593,6 +623,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.
diff --git a/test/gourdinl/postpass_exp.c b/test/gourdinl/postpass_exp.c
index 522ac2a6..bc234091 100644
--- a/test/gourdinl/postpass_exp.c
+++ b/test/gourdinl/postpass_exp.c
@@ -1,5 +1,11 @@
-int main(int x, int y) {
-  int z = x << 32;
+long foo(int x, char y, long *t) {
+  int z = x / 4096;
+  y = x / 256;
+  t[0] = t[1] * t[2];
+  if (x + z < 7) {
+    if (y < 7)
+      return 421 + t[0];
+  }
   y = y - z;
-  return x + y;
+  return x + y - t[0];
 }