Extend offline for new prims

UQ-PAC · Jan 17, 2025 · c6c51f0 · c6c51f0
1 parent da42348
commit c6c51f0
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 0 deletions.
diff --git a/offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp b/offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp
@@ -489,6 +489,8 @@ class llvm_run_time_interface : virtual public lifter_interface<llvm_lifter_trai
   rt_expr f_gen_FPRecpX(rt_expr x, rt_expr fpcr) override { assert(0); }
   rt_expr f_gen_FPSqrt(rt_expr x, rt_expr fpcr) override { assert(0); }
   rt_expr f_gen_FPRecipEstimate(rt_expr x, rt_expr fpcr) override { assert(0); }
+  rt_expr f_gen_UnsignedRSqrtEstimate(rt_expr x) override { assert(0); }
+  rt_expr f_gen_FPRSqrtEstimate(rt_expr x, rt_expr fpcr) override { assert(0); }
   rt_expr f_gen_BFAdd(rt_expr x, rt_expr y) override { assert(0); }
   rt_expr f_gen_BFMul(rt_expr x, rt_expr y) override { assert(0); }
   rt_expr f_gen_FPConvertBF(rt_expr x, rt_expr fpcr, rt_expr rounding) override { assert(0); }

diff --git a/offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp b/offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp
@@ -168,6 +168,8 @@ template <typename Traits> class lifter_interface : public Traits {
   virtual rt_expr f_gen_FPRecpX(rt_expr x, rt_expr fpcr) = 0;
   virtual rt_expr f_gen_FPSqrt(rt_expr x, rt_expr fpcr) = 0;
   virtual rt_expr f_gen_FPRecipEstimate(rt_expr x, rt_expr fpcr) = 0;
+  virtual rt_expr f_gen_UnsignedRSqrtEstimate(rt_expr x) = 0;
+  virtual rt_expr f_gen_FPRSqrtEstimate(rt_expr x, rt_expr fpcr) = 0;
   virtual rt_expr f_gen_BFAdd(rt_expr x, rt_expr y) = 0;
   virtual rt_expr f_gen_BFMul(rt_expr x, rt_expr y) = 0;
   virtual rt_expr f_gen_FPConvertBF(rt_expr x, rt_expr fpcr,

diff --git a/offlineASL-scala/lifter/src/interface.scala b/offlineASL-scala/lifter/src/interface.scala
@@ -55,6 +55,8 @@ trait LiftState[RTSym, RTLabel, BV <: RTSym] {
   def f_gen_FPMulX(targ0: BigInt, arg0: RTSym, arg1: RTSym, arg2: RTSym): RTSym
   def f_gen_FPRSqrtStepFused(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
   def f_gen_FPRecipEstimate(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
+  def f_gen_UnsignedRSqrtEstimate(targ0: BigInt, arg0: RTSym): RTSym 
+  def f_gen_FPRSqrtEstimate(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
   def f_gen_FPRecipStepFused(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
   def f_gen_FPRecpX(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
   def f_gen_FPRoundInt(targ0: BigInt, arg0: RTSym, arg1: RTSym, arg2: RTSym, arg3: RTSym): RTSym

diff --git a/offlineASL-scala/main/src/NoneLifter.scala b/offlineASL-scala/main/src/NoneLifter.scala
@@ -66,6 +66,8 @@ class NotImplementedLifter extends LiftState[RExpr, String, BitVec] {
   def f_gen_FPMulX(targ0: BigInt, arg0: RTSym, arg1: RTSym, arg2: RTSym): RTSym = throw NotImplementedError()
   def f_gen_FPRSqrtStepFused(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
   def f_gen_FPRecipEstimate(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
+  def f_gen_UnsignedRSqrtEstimate(targ0: BigInt, arg0: RTSym): RTSym = throw NotImplementedError()
+  def f_gen_FPRSqrtEstimate(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
   def f_gen_FPRecipStepFused(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
   def f_gen_FPRecpX(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
   def f_gen_FPRoundInt(targ0: BigInt, arg0: RTSym, arg1: RTSym, arg2: RTSym, arg3: RTSym): RTSym = throw NotImplementedError()

diff --git a/offlineASL/offline_utils.ml b/offlineASL/offline_utils.ml
@@ -290,6 +290,10 @@ let f_gen_FPSqrt w x t =
   Expr_TApply (FIdent ("FPSqrt", 0), [expr_of_z w], [x; t])
 let f_gen_FPRecipEstimate w x r =
   Expr_TApply (FIdent ("FPRecipEstimate", 0), [expr_of_z w], [x; r])
+let f_gen_UnsignedRSqrtEstimate w x =
+  Expr_TApply (FIdent ("UnsignedRSqrtEstimate", 0), [expr_of_z w], [x])
+let f_gen_FPRSqrtEstimate w x r =
+  Expr_TApply (FIdent ("FPRSqrtEstimate", 0), [expr_of_z w], [x; r])
 
 let f_gen_BFAdd x y =
   Expr_TApply (FIdent ("BFAdd", 0), [], [x; y])