fix: re-add threading

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"

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"] }

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<AssignmentModel<ModeledBlock>> for PythonAssignmentModel {
 #[pymethods]
 impl PythonAssignmentModel {
     fn eval_bv(&self, bv: Py<PyAny>, model_completion: bool) -> PyResult<Py<PyAny>> {
-        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<PythonState> {

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<Self>) -> Option<(String, Py<PyAny>)> {
-        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,
+            }
+        })
     }
 }

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<Mutex<()>> = Arc::new(Mutex::new(()));
+}
+
 #[pyclass(name = "SynthesisParams")]
 #[derive(Clone)]
 pub struct PythonSynthesisParams {
@@ -25,8 +29,8 @@ impl PythonSynthesisParams {
     pub fn run(&self) -> PyResult<PythonDecisionResult> {
         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<PyAny>) {
-        let closure: Arc<PythonStateConstraintGenerator> = Arc::new(move |_, s, a| {
-            let state = PythonState::from(s.clone());
-            Python::with_gil(|py| {
+        let closure: Arc<PythonStateConstraintGenerator> = 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<StateConstraintGenerator> =
-            unsafe { std::mem::transmute(closure) };
+        let transmuted_closure: Arc<StateConstraintGenerator> = closure;
         self.inner.preconditions.push(transmuted_closure);
     }
 
     pub fn add_postcondition(&mut self, obj: Py<PyAny>) {
-        let closure: Arc<PythonStateConstraintGenerator> = Arc::new(move |_, s, a| {
-            let state = PythonState::from(s.clone());
-            Python::with_gil(|py| {
+        let closure: Arc<PythonStateConstraintGenerator> = 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<StateConstraintGenerator> =
-            unsafe { std::mem::transmute(closure) };
+        let transmuted_closure: Arc<StateConstraintGenerator> = closure;
         self.inner.postconditions.push(transmuted_closure);
     }
 
     pub fn add_transition_constraint(&mut self, obj: Py<PyAny>) {
-        let closure: Arc<PythonTransitionConstraintGenerator> = Arc::new(move |_, b| {
-            let block = PythonModeledBlock { instr: b.clone() };
-            Python::with_gil(|py| {
+        let closure: Arc<PythonTransitionConstraintGenerator> = 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<TransitionConstraintGenerator> =
-            unsafe { std::mem::transmute(closure) };
+        let transmuted_closure: Arc<TransitionConstraintGenerator> = closure;
         self.inner.pointer_invariants.push(transmuted_closure);
     }
 }
 
 pub type PythonStateConstraintGenerator =
-    dyn Fn(&JingleContext, &State, u64) -> Result<Bool, CrackersError> + Send + Sync + 'static;
+    dyn Fn(&State, u64) -> Result<Bool, CrackersError> + Send + Sync + 'static;
 
-pub type PythonTransitionConstraintGenerator = dyn Fn(&JingleContext, &ModeledBlock) -> Result<Option<Bool>, CrackersError>
-    + Send
-    + Sync
-    + 'static;
+pub type PythonTransitionConstraintGenerator =
+    dyn Fn(&ModeledBlock) -> Result<Option<Bool>, CrackersError> + Send + Sync + 'static;