abs builtins

1 files changed, 20 insertions, 0 deletions

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.