From 682a18bfa9be31c7e9b52f03e875d49035dc80d1 Mon Sep 17 00:00:00 2001
From: Kevin Phoenix <kevin@kphoenix.us>
Date: Mon, 4 Nov 2024 17:16:29 -0700
Subject: [PATCH] Add support for creating BVVs from negative python ints

---
 crates/clarirs_py/src/ast/bv.rs | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/crates/clarirs_py/src/ast/bv.rs b/crates/clarirs_py/src/ast/bv.rs
index 5b7b6cc..dbabe49 100644
--- a/crates/clarirs_py/src/ast/bv.rs
+++ b/crates/clarirs_py/src/ast/bv.rs
@@ -5,7 +5,7 @@ use std::sync::LazyLock;
 
 use clarirs_core::ast::bitvec::BitVecExt;
 use dashmap::DashMap;
-use num_bigint::BigUint;
+use num_bigint::{BigInt, BigUint};
 use pyo3::exceptions::{PyTypeError, PyValueError};
 use pyo3::types::{PyBytes, PyFrozenSet, PyWeakrefReference};
 
@@ -474,6 +474,21 @@ pub fn BVV(py: Python, value: Bound<PyAny>, size: Option<u32>) -> Result<Py<BV>,
             return Err(PyErr::new::<PyValueError, _>("size must be specified"));
         }
     }
+    if let Ok(int_val) = value.extract::<BigInt>() {
+        if let Some(size) = size {
+            let uint_value = int_val.to_biguint().unwrap_or(
+                ((BigInt::from(1) << (size - 1)) + int_val)
+                    .to_biguint()
+                    .expect("BigInt to BigUInt failed"),
+            );
+            let a = GLOBAL_CONTEXT
+                .bvv_from_biguint_with_size(&uint_value, size)
+                .map_err(ClaripyError::from)?;
+            return Ok(BV::new(py, &a)?);
+        } else {
+            return Err(PyErr::new::<PyValueError, _>("size must be specified"));
+        }
+    }
     // TODO: deduplicate bytes/str
     if let Ok(bytes_val) = value.extract::<Vec<u8>>() {
         let int_val = BigUint::from_bytes_le(&bytes_val);