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

1 files changed, 35 insertions, 0 deletions

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.