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

1 files changed, 20 insertions, 0 deletions

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.