From c6c51f0322592bacb711b061f31a185e5d20ea04 Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Fri, 17 Jan 2025 12:29:39 +1000 Subject: [PATCH] Extend offline for new prims --- .../aslp-lifter-llvm/include/aslp/llvm_interface.hpp | 2 ++ .../subprojects/aslp-lifter/include/aslp/interface.hpp | 2 ++ offlineASL-scala/lifter/src/interface.scala | 2 ++ offlineASL-scala/main/src/NoneLifter.scala | 2 ++ offlineASL/offline_utils.ml | 4 ++++ 5 files changed, 12 insertions(+) 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 index 13401a78..03358cb7 100644 --- 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 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 index 006cacd2..077a36f6 100644 --- 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 index 30b47a15..e82d471d 100644 --- 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 index 0130a5d7..d0755924 100644 --- 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])