Add missing ops and improve claripy compatibiliy

twizmwazin · Oct 30, 2024 · b49350a · b49350a
1 parent 101d9be
commit b49350a
Show file tree

Hide file tree

Showing 5 changed files with 86 additions and 21 deletions.
diff --git a/crates/clarirs_py/src/ast/bv.rs b/crates/clarirs_py/src/ast/bv.rs
@@ -125,8 +125,30 @@ binop!(Pow, pow, BV, BV, BV);
 binop!(ShL, ashl, BV, BV, BV);
 binop!(LShR, lshr, BV, BV, BV);
 binop!(AShR, ashr, BV, BV, BV);
+binop!(RotateLeft, rotate_left, BV, BV, BV);
+binop!(RotateRight, rotate_right, BV, BV, BV);
 binop!(Concat, concat, BV, BV, BV);
 
+#[pyfunction]
+pub fn Extract(py: Python, base: Bound<BV>, start: u32, end: u32) -> Result<Py<BV>, ClaripyError> {
+    BV::new(py, GLOBAL_CONTEXT.extract(&base.get().inner, start, end)?)
+}
+
+#[pyfunction]
+pub fn ZeroExt(py: Python, base: Bound<BV>, amount: u32) -> Result<Py<BV>, ClaripyError> {
+    BV::new(py, GLOBAL_CONTEXT.zero_ext(&base.get().inner, amount)?)
+}
+
+#[pyfunction]
+pub fn SignExt(py: Python, base: Bound<BV>, amount: u32) -> Result<Py<BV>, ClaripyError> {
+    BV::new(py, GLOBAL_CONTEXT.sign_ext(&base.get().inner, amount)?)
+}
+
+#[pyfunction]
+pub fn Reverse(py: Python, base: Bound<BV>) -> Result<Py<BV>, ClaripyError> {
+    BV::new(py, GLOBAL_CONTEXT.reverse(&base.get().inner)?)
+}
+
 binop!(ULT, ult, Bool, BV, BV);
 binop!(ULE, ule, Bool, BV, BV);
 binop!(UGT, ugt, Bool, BV, BV);
@@ -138,11 +160,6 @@ binop!(SGE, sge, Bool, BV, BV);
 binop!(Eq_, eq_, Bool, BV, BV);
 binop!(Neq, neq, Bool, BV, BV);
 
-#[pyfunction]
-pub fn Extract(py: Python, base: Bound<BV>, start: u32, end: u32) -> Result<Py<BV>, ClaripyError> {
-    BV::new(py, GLOBAL_CONTEXT.extract(&base.get().inner, start, end)?)
-}
-
 #[pyfunction]
 pub fn If(
     py: Python,
@@ -160,8 +177,41 @@ pub(crate) fn import(_: Python, m: &Bound<PyModule>) -> PyResult<()> {
     m.add_class::<BV>()?;
 
     add_pyfunctions!(
-        m, BVS, BVV, Not, And, Or, Xor, Add, Sub, Mul, UDiv, SDiv, UMod, SMod, Pow, ShL, LShR,
-        AShR, Concat, Extract, ULT, ULE, UGT, UGE, SLT, SLE, SGT, SGE, Eq_, If,
+        m,
+        BVS,
+        BVV,
+        Not,
+        And,
+        Or,
+        Xor,
+        Add,
+        Sub,
+        Mul,
+        UDiv,
+        SDiv,
+        UMod,
+        SMod,
+        Pow,
+        ShL,
+        LShR,
+        AShR,
+        RotateLeft,
+        RotateRight,
+        Concat,
+        Extract,
+        ZeroExt,
+        SignExt,
+        Reverse,
+        ULT,
+        ULE,
+        UGT,
+        UGE,
+        SLT,
+        SLE,
+        SGT,
+        SGE,
+        Eq_,
+        If,
     );
 
     Ok(())

diff --git a/crates/clarirs_py/src/ast/fp.rs b/crates/clarirs_py/src/ast/fp.rs
@@ -102,6 +102,11 @@ pub fn FPV(py: Python, value: f64, sort: PyFSort) -> Result<Py<FP>, ClaripyError
     )
 }
 
+#[pyfunction]
+pub fn fpFP(py: Python, sign: Bound<BV>, exponent: Bound<BV>, significand: Bound<BV>) -> Result<Py<FP>, ClaripyError> {
+    todo!()
+}
+
 #[pyfunction(name = "fpToFP", signature = (fp, sort, rm = None))]
 pub fn FpToFP(
     py: Python,
@@ -115,7 +120,7 @@ pub fn FpToFP(
     )
 }
 
-#[pyfunction(name = "bvToFpUnsigned", signature = (bv, sort, rm = None))]
+#[pyfunction(name = "fpToFPUnsigned", signature = (bv, sort, rm = None))]
 pub fn BvToFpUnsigned(
     py: Python,
     bv: Bound<BV>,
@@ -235,7 +240,7 @@ pub fn FpSqrt(py: Python, lhs: Bound<FP>, rm: Option<PyRM>) -> Result<Py<FP>, Cl
     )
 }
 
-#[pyfunction(name = "FpEq", signature = (lhs, rhs))]
+#[pyfunction(name = "fpEQ", signature = (lhs, rhs))]
 pub fn FpEq(py: Python, lhs: Bound<FP>, rhs: Bound<FP>) -> Result<Py<Bool>, ClaripyError> {
     Bool::new(
         py,
@@ -251,39 +256,39 @@ pub fn FpNeq(py: Python, lhs: Bound<FP>, rhs: Bound<FP>) -> Result<Py<Bool>, Cla
     )
 }
 
-#[pyfunction(name = "fpLt", signature = (lhs, rhs))]
+#[pyfunction(name = "fpLT", signature = (lhs, rhs))]
 pub fn FpLt(py: Python, lhs: Bound<FP>, rhs: Bound<FP>) -> Result<Py<Bool>, ClaripyError> {
     Bool::new(
         py,
         GLOBAL_CONTEXT.fp_lt(&lhs.get().inner, &rhs.get().inner)?,
     )
 }
 
-#[pyfunction(name = "fpLeq", signature = (lhs, rhs))]
+#[pyfunction(name = "fpLEQ", signature = (lhs, rhs))]
 pub fn FpLeq(py: Python, lhs: Bound<FP>, rhs: Bound<FP>) -> Result<Py<Bool>, ClaripyError> {
     Bool::new(
         py,
         GLOBAL_CONTEXT.fp_leq(&lhs.get().inner, &rhs.get().inner)?,
     )
 }
 
-#[pyfunction(name = "fpGt", signature = (lhs, rhs))]
+#[pyfunction(name = "fpGT", signature = (lhs, rhs))]
 pub fn FpGt(py: Python, lhs: Bound<FP>, rhs: Bound<FP>) -> Result<Py<Bool>, ClaripyError> {
     Bool::new(
         py,
         GLOBAL_CONTEXT.fp_gt(&lhs.get().inner, &rhs.get().inner)?,
     )
 }
 
-#[pyfunction(name = "fpGeq", signature = (lhs, rhs))]
+#[pyfunction(name = "fpGEQ", signature = (lhs, rhs))]
 pub fn FpGeq(py: Python, lhs: Bound<FP>, rhs: Bound<FP>) -> Result<Py<Bool>, ClaripyError> {
     Bool::new(
         py,
         GLOBAL_CONTEXT.fp_geq(&lhs.get().inner, &rhs.get().inner)?,
     )
 }
 
-#[pyfunction(name = "fpIsNan", signature = (fp))]
+#[pyfunction(name = "fpIsNaN", signature = (fp))]
 pub fn FpIsNan(py: Python, fp: Bound<FP>) -> Result<Py<Bool>, ClaripyError> {
     Bool::new(py, GLOBAL_CONTEXT.fp_is_nan(&fp.get().inner)?)
 }
@@ -301,6 +306,7 @@ pub(crate) fn import(_: Python, m: &Bound<PyModule>) -> PyResult<()> {
         m,
         FPS,
         FPV,
+        fpFP,
         FpToFP,
         BvToFpUnsigned,
         fpToIEEEBV,

diff --git a/crates/clarirs_py/src/ast/mod.rs b/crates/clarirs_py/src/ast/mod.rs
@@ -184,5 +184,7 @@ pub(crate) fn import(py: Python, m: &Bound<PyModule>) -> PyResult<()> {
     m.add_class::<bv::BV>()?;
     m.add_class::<fp::FP>()?;
     m.add_class::<string::PyAstString>()?;
+    m.add_function(wrap_pyfunction!(bool::true_op, m)?)?;
+    m.add_function(wrap_pyfunction!(bool::false_op, m)?)?;
     Ok(())
 }
diff --git a/crates/clarirs_py/src/ast/string.rs b/crates/clarirs_py/src/ast/string.rs
@@ -149,12 +149,12 @@ pub fn StrSuffixOf(
 }
 
 #[pyfunction]
-pub fn StrToBV(py: Python, s: Bound<PyAstString>) -> Result<Py<BV>, ClaripyError> {
+pub fn StrToInt(py: Python, s: Bound<PyAstString>) -> Result<Py<BV>, ClaripyError> {
     BV::new(py, GLOBAL_CONTEXT.strtobv(&s.get().inner)?)
 }
 
 #[pyfunction]
-pub fn BVToStr(py: Python, bv: Bound<BV>) -> Result<Py<PyAstString>, ClaripyError> {
+pub fn IntToStr(py: Python, bv: Bound<BV>) -> Result<Py<PyAstString>, ClaripyError> {
     PyAstString::new(py, GLOBAL_CONTEXT.bvtostr(&bv.get().inner)?)
 }
 
@@ -194,8 +194,8 @@ pub(crate) fn import(_: Python, m: &Bound<PyModule>) -> PyResult<()> {
         StrReplace,
         StrPrefixOf,
         StrSuffixOf,
-        StrToBV,
-        BVToStr,
+        StrToInt,
+        IntToStr,
         StrIsDigit,
         StrEq,
         StrNeq,

diff --git a/crates/clarirs_py/src/lib.rs b/crates/clarirs_py/src/lib.rs
@@ -98,8 +98,13 @@ pub fn clarirs(py: Python, m: &Bound<'_, PyModule>) -> PyResult<()> {
         ast::bv::ShL,
         ast::bv::LShR,
         ast::bv::AShR,
+        ast::bv::RotateLeft,
+        ast::bv::RotateRight,
         ast::bv::Concat,
         ast::bv::Extract,
+        ast::bv::ZeroExt,
+        ast::bv::SignExt,
+        ast::bv::Reverse,
         ast::bv::Eq_,
         ast::bv::Neq,
         ast::bv::ULT,
@@ -113,6 +118,7 @@ pub fn clarirs(py: Python, m: &Bound<'_, PyModule>) -> PyResult<()> {
         // FP
         ast::fp::FPS,
         ast::fp::FPV,
+        ast::fp::fpFP,
         ast::fp::FpToFP,
         ast::fp::BvToFpUnsigned,
         ast::fp::fpToIEEEBV,
@@ -146,8 +152,8 @@ pub fn clarirs(py: Python, m: &Bound<'_, PyModule>) -> PyResult<()> {
         ast::string::StrReplace,
         ast::string::StrPrefixOf,
         ast::string::StrSuffixOf,
-        ast::string::StrToBV,
-        ast::string::BVToStr,
+        ast::string::StrToInt,
+        ast::string::IntToStr,
         ast::string::StrIsDigit,
         ast::string::StrEq,
         ast::string::StrNeq,
@@ -184,11 +190,12 @@ pub fn clarirs(py: Python, m: &Bound<'_, PyModule>) -> PyResult<()> {
     // Compat
 
     // fp
-    let fp = PyModule::new_bound(py, "fp")?;
+    let fp = PyModule::new_bound(py, "clarirs.fp")?;
     fp.add_class::<ast::fp::PyRM>()?;
     fp.add_class::<ast::fp::PyFSort>()?;
     fp.add("FSORT_FLOAT", ast::fp::fsort_float())?;
     fp.add("FSORT_DOUBLE", ast::fp::fsort_double())?;
+    pyo3::py_run!(py, fp, "import sys; sys.modules['clarirs.fp'] = fp");
     m.add_submodule(&fp)?;
 
     Ok(())