Skip to content

Commit

Permalink
Add support for creating BVVs from negative python ints
Browse files Browse the repository at this point in the history
  • Loading branch information
twizmwazin committed Nov 5, 2024
1 parent 99ab6bc commit 682a18b
Showing 1 changed file with 16 additions and 1 deletion.
17 changes: 16 additions & 1 deletion crates/clarirs_py/src/ast/bv.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};

Expand Down Expand Up @@ -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);
Expand Down

0 comments on commit 682a18b

Please sign in to comment.