abs builtins

6 files changed, 132 insertions, 18 deletions

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 434d283e..c493f708 100644
--- a/kvx/ExtValues.v
+++ b/kvx/ExtValues.v
@@ -21,14 +21,14 @@ Require Import Lia.
 
 Open Scope Z_scope.
 
-Definition int_abs_diff (x y : Z) := Z.abs (x - y).
-Definition int_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 int_abs_diff2_correct :
-  forall x y : Z, (int_abs_diff x y) = (int_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 int_abs_diff, int_abs_diff2.
+  unfold Z_abs_diff, Z_abs_diff2.
   unfold Z.leb.
   pose proof (Z.compare_spec x y) as Hspec.
   inv Hspec.
@@ -755,20 +755,47 @@ 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 :=
+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 (Int.repr (f (Int.signed i1) (Int.signed i2)))
+  | (Vint i1), (Vint i2) => Vint (f i1 i2)
   |  _, _ => Vundef
   end.
 
-Definition double_op_longZ f v1 v2 :=
+Definition double_op_long f v1 v2 :=
   match v1, v2 with
-  | (Vlong i1), (Vlong i2) => Vlong (Int64.repr (f (Int64.signed i1) (Int64.signed i2)))
+  | (Vlong i1), (Vlong i2) => Vlong (f i1 i2)
   | _, _ => Vundef
   end.
 
-Definition absdiff := double_op_intZ int_abs_diff.
-Definition absdiffl := double_op_longZ int_abs_diff.
+Definition absdiff := double_op_int int_absdiff.
+Definition absdiffl := double_op_long long_absdiff.
 
 Definition abs v1 :=
   match v1 with
@@ -786,7 +813,7 @@ 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.
+  f_equal. unfold int_absdiff, Z_abs_diff.
   change (Int.unsigned Int.zero) with 0%Z.
   rewrite Z.sub_0_r.
   reflexivity.
@@ -796,7 +823,7 @@ 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.
+  f_equal. unfold long_absdiff, Z_abs_diff.
   change (Int64.unsigned Int64.zero) with 0%Z.
   rewrite Z.sub_0_r.
   reflexivity.
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/ValueAOp.v b/kvx/ValueAOp.v
index f0fed567..ddfe94f3 100644
--- a/kvx/ValueAOp.v
+++ b/kvx/ValueAOp.v
@@ -157,10 +157,10 @@ Definition eval_static_insfl stop start prev fld :=
   else Vtop.
 
 Definition absdiff := binop_int
-   (fun i1 i2 => Int.repr (ExtValues.int_abs_diff (Int.signed i1) (Int.signed i2))).
+   (fun i1 i2 => ExtValues.int_absdiff i1 i2).
 
 Definition absdiffl := binop_long
-   (fun i1 i2 => Int64.repr (ExtValues.int_abs_diff (Int64.signed i1) (Int64.signed i2))).
+   (fun i1 i2 => ExtValues.long_absdiff i1 i2).
               
 Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   match op, vl with