begin adding abdw abdd

9 files changed, 180 insertions, 8 deletions

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/Asmvliw.v b/kvx/Asmvliw.v
index 45b230e6..bbd40692 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.absdiff v (Vlong i)
   end.
 
 Definition cmove bt v1 v2 v3 :=
diff --git a/kvx/ExtValues.v b/kvx/ExtValues.v
index b4e14898..434d283e 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 int_abs_diff (x y : Z) := Z.abs (x - y).
+Definition int_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 int_abs_diff2_correct :
+  forall x y : Z, (int_abs_diff x y) = (int_abs_diff2 x y).
 Proof.
   intros.
-  unfold abs_diff, abs_diff2.
+  unfold int_abs_diff, int_abs_diff2.
   unfold Z.leb.
   pose proof (Z.compare_spec x y) as Hspec.
   inv Hspec.
@@ -754,3 +754,72 @@ 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 double_op_intZ f v1 v2 :=
+  match v1, v2 with
+  | (Vint i1), (Vint i2) => Vint (Int.repr (f (Int.signed i1) (Int.signed i2)))
+  |  _, _ => Vundef
+  end.
+
+Definition double_op_longZ f v1 v2 :=
+  match v1, v2 with
+  | (Vlong i1), (Vlong i2) => Vlong (Int64.repr (f (Int64.signed i1) (Int64.signed i2)))
+  | _, _ => Vundef
+  end.
+
+Definition absdiff := double_op_intZ int_abs_diff.
+Definition absdiffl := double_op_longZ int_abs_diff.
+
+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_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 int_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/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 47849dd5..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
@@ -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/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..f0fed567 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 => Int.repr (ExtValues.int_abs_diff (Int.signed i1) (Int.signed i2))).
+
+Definition absdiffl := binop_long
+   (fun i1 i2 => Int64.repr (ExtValues.int_abs_diff (Int64.signed i1) (Int64.signed 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.