diff --git a/crackers/Cargo.toml b/crackers/Cargo.toml index 4af03de..4451592 100644 --- a/crackers/Cargo.toml +++ b/crackers/Cargo.toml @@ -24,7 +24,7 @@ toml = ["dep:toml_edit"] z3-gh-release = ["z3/gh-release"] [dependencies] -jingle = { version = "0.2.3", features = ["gimli"] } +jingle = { version = "0.2.4", features = ["gimli"] } z3 = "0.16.0" serde = { version = "1.0.203", features = ["derive"] } thiserror = "2.0" diff --git a/crackers_python/Cargo.toml b/crackers_python/Cargo.toml index cb241ec..3ccb862 100644 --- a/crackers_python/Cargo.toml +++ b/crackers_python/Cargo.toml @@ -12,10 +12,11 @@ crate-type = ["cdylib"] [dependencies] pyo3 = { version = "0.25", features = ["extension-module", "py-clone"] } crackers = {path = "../crackers", features = ["pyo3"], version = "0.5.0" } -jingle = {version = "0.2.3", features = ["pyo3"]} +jingle = { version="0.2.4", features = ["pyo3"]} toml_edit = "0.22.22" z3 = "0.16.0" serde_json = "1.0.140" +lazy_static = "1.5.0" [dev-dependencies] pyo3 = { version = "0", features = ["extension-module"] } diff --git a/crackers_python/src/decision/assignment_model/mod.rs b/crackers_python/src/decision/assignment_model/mod.rs index 93ed41d..1257c7e 100644 --- a/crackers_python/src/decision/assignment_model/mod.rs +++ b/crackers_python/src/decision/assignment_model/mod.rs @@ -11,7 +11,7 @@ use jingle::python::z3::ast::PythonAst; use jingle::sleigh::{ArchInfoProvider, SpaceType}; use jingle::varnode::{ResolvedIndirectVarNode, ResolvedVarnode}; use pyo3::exceptions::PyRuntimeError; -use pyo3::{Py, PyAny, PyErr, PyResult, pyclass, pymethods}; +use pyo3::{Py, PyAny, PyErr, PyResult, Python, pyclass, pymethods}; use std::rc::Rc; use z3::ast::BV; @@ -77,13 +77,15 @@ impl TryFrom> for PythonAssignmentModel { #[pymethods] impl PythonAssignmentModel { fn eval_bv(&self, bv: Py, model_completion: bool) -> PyResult> { - let bv = BV::try_from_python(bv)?; - let val = self - .inner - .model() - .eval(&bv, model_completion) - .ok_or(PyRuntimeError::new_err("Could not eval model"))?; - val.try_into_python() + Python::with_gil(|py| { + let bv = BV::try_from_python(bv, py)?; + let val = self + .inner + .model() + .eval(&bv, model_completion) + .ok_or(PyRuntimeError::new_err("Could not eval model"))?; + val.try_into_python(py) + }) } pub fn initial_state(&self) -> Option { diff --git a/crackers_python/src/decision/assignment_model/model_varnode_iterator.rs b/crackers_python/src/decision/assignment_model/model_varnode_iterator.rs index 8ca17b1..0ef40eb 100644 --- a/crackers_python/src/decision/assignment_model/model_varnode_iterator.rs +++ b/crackers_python/src/decision/assignment_model/model_varnode_iterator.rs @@ -1,5 +1,5 @@ use jingle::python::z3::ast::PythonAst; -use pyo3::{Py, PyAny, PyRef, PyRefMut, pyclass, pymethods}; +use pyo3::{Py, PyAny, PyRef, PyRefMut, Python, pyclass, pymethods}; use z3::ast::BV; #[pyclass(unsendable)] @@ -20,10 +20,12 @@ impl ModelVarNodeIterator { } pub fn __next__(mut slf: PyRefMut) -> Option<(String, Py)> { - let (name, bv) = slf.vn.next()?; - match bv.try_into_python() { - Ok(bv) => Some((name, bv)), - _ => None, - } + Python::with_gil(|py| { + let (name, bv) = slf.vn.next()?; + match bv.try_into_python(py) { + Ok(bv) => Some((name, bv)), + _ => None, + } + }) } } diff --git a/crackers_python/src/synthesis.rs b/crackers_python/src/synthesis.rs index 1859c61..bd9bc65 100644 --- a/crackers_python/src/synthesis.rs +++ b/crackers_python/src/synthesis.rs @@ -5,15 +5,19 @@ use crackers::synthesis::DecisionResult; use crackers::synthesis::builder::{ StateConstraintGenerator, SynthesisParams, TransitionConstraintGenerator, }; -use jingle::JingleContext; use jingle::modeling::{ModeledBlock, State}; use jingle::python::modeled_block::PythonModeledBlock; use jingle::python::state::PythonState; use jingle::python::z3::ast::PythonAst; +use lazy_static::lazy_static; use pyo3::{Py, PyAny, PyResult, Python, pyclass, pymethods}; -use std::sync::Arc; +use std::sync::{Arc, Mutex}; use z3::ast::Bool; +lazy_static! { + static ref MUTEX: Arc> = Arc::new(Mutex::new(())); +} + #[pyclass(name = "SynthesisParams")] #[derive(Clone)] pub struct PythonSynthesisParams { @@ -25,8 +29,8 @@ impl PythonSynthesisParams { pub fn run(&self) -> PyResult { let res = Python::with_gil(|py| { py.allow_threads(|| match self.inner.combine_instructions { - false => self.inner.build_single()?.decide_single_threaded(), - true => self.inner.build_combined()?.decide_single_threaded(), + false => self.inner.build_single()?.decide(), + true => self.inner.build_combined()?.decide(), }) })?; match res { @@ -40,56 +44,61 @@ impl PythonSynthesisParams { } pub fn add_precondition(&mut self, obj: Py) { - let closure: Arc = Arc::new(move |_, s, a| { - let state = PythonState::from(s.clone()); - Python::with_gil(|py| { + let closure: Arc = Arc::new(move |s, a| { + let g = MUTEX.lock().unwrap(); + let r = Python::with_gil(|py| { + let state = PythonState::from(s.clone()); let res = obj.call(py, (state, a), None)?; - let bool = Bool::try_from_python(res).map_err(CrackersError::PythonError)?; + let bool = Bool::try_from_python(res, py).map_err(CrackersError::PythonError)?; Ok(bool) - }) + }); + drop(g); + r }); - let transmuted_closure: Arc = - unsafe { std::mem::transmute(closure) }; + let transmuted_closure: Arc = closure; self.inner.preconditions.push(transmuted_closure); } pub fn add_postcondition(&mut self, obj: Py) { - let closure: Arc = Arc::new(move |_, s, a| { - let state = PythonState::from(s.clone()); - Python::with_gil(|py| { + let closure: Arc = Arc::new(move |s, a| { + let g = MUTEX.lock().unwrap(); + let r = Python::with_gil(|py| { + let state = PythonState::from(s.clone()); let res = obj.call(py, (state, a), None)?; - let bool = Bool::try_from_python(res).map_err(CrackersError::PythonError)?; + let bool = Bool::try_from_python(res, py).map_err(CrackersError::PythonError)?; Ok(bool) - }) + }); + drop(g); + r }); - let transmuted_closure: Arc = - unsafe { std::mem::transmute(closure) }; + let transmuted_closure: Arc = closure; self.inner.postconditions.push(transmuted_closure); } pub fn add_transition_constraint(&mut self, obj: Py) { - let closure: Arc = Arc::new(move |_, b| { - let block = PythonModeledBlock { instr: b.clone() }; - Python::with_gil(|py| { + let closure: Arc = Arc::new(move |b| { + let g = MUTEX.lock().unwrap(); + let r = Python::with_gil(|py| { + let block = PythonModeledBlock { instr: b.clone() }; let res = obj.call(py, (block,), None)?; if res.is_none(py) { Ok(None) } else { - let bool = Bool::try_from_python(res).map_err(CrackersError::PythonError)?; + let bool = + Bool::try_from_python(res, py).map_err(CrackersError::PythonError)?; Ok(Some(bool)) } - }) + }); + drop(g); + r }); - let transmuted_closure: Arc = - unsafe { std::mem::transmute(closure) }; + let transmuted_closure: Arc = closure; self.inner.pointer_invariants.push(transmuted_closure); } } pub type PythonStateConstraintGenerator = - dyn Fn(&JingleContext, &State, u64) -> Result + Send + Sync + 'static; + dyn Fn(&State, u64) -> Result + Send + Sync + 'static; -pub type PythonTransitionConstraintGenerator = dyn Fn(&JingleContext, &ModeledBlock) -> Result, CrackersError> - + Send - + Sync - + 'static; +pub type PythonTransitionConstraintGenerator = + dyn Fn(&ModeledBlock) -> Result, CrackersError> + Send + Sync + 'static;