build fix; whole api chain works, just need to make it more useful now

Author: toolCHAINZ

crackers/src/synthesis/assignment_model.rs

@@ -63,7 +63,6 @@ impl<'ctx, T: ModelingContext<'ctx>> AssignmentModel<'ctx, T> {
 
 impl<'ctx, T: ModelingContext<'ctx> + Display> Display for AssignmentModel<'ctx, T> {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
-        dbg!("hello");
         writeln!(f, "Gadgets:\n")?;
         for block in &self.gadgets {
             writeln!(f, "{}\n", block)?;

crackers/src/synthesis/mod.rs

@@ -1,4 +1,4 @@
-use jingle::modeling::{ModeledBlock, ModeledInstruction, ModelingContext};
+use jingle::modeling::{ModeledBlock, ModeledInstruction, ModelingContext, State};
 use jingle::sleigh::Instruction;
 use jingle::JingleContext;
 use std::cmp::Ordering;
@@ -183,7 +183,6 @@ impl<'ctx> AssignmentSynthesis<'ctx> {
                                     "Theory returned SAT for {:?}!",
                                     response.assignment
                                 );
-                                dbg!("Terminating remaining workers");
                                 req_channels.clear();
                                 for x in &kill_senders {
                                     x.send(()).unwrap();
@@ -193,11 +192,11 @@ impl<'ctx> AssignmentSynthesis<'ctx> {
                                 let jingle = JingleContext::new(self.z3, self.library.as_ref());
                                 let a: PcodeAssignment<'ctx> =
                                     t.build_assignment(&jingle, response.assignment)?;
-                                dbg!("Workers Terminated; building and checking model");
+                                event!(Level::DEBUG, "Workers Terminated; building and checking model");
                                 let solver = Solver::new(self.z3);
                                 let jingle = JingleContext::new(self.z3, self.library.as_ref());
                                 let model = a.check(&jingle, &solver)?;
-                                dbg!("Model built");
+                                event!(Level::DEBUG, "Model built");
                                 return Ok(DecisionResult::AssignmentFound(model));
                             }
                             Some(c) => {

crackers_python/Cargo.toml

@@ -13,6 +13,8 @@ pyo3 = { version = "0.24", features = ["extension-module", "py-clone"] }
 crackers = {path = "../crackers", features = ["pyo3"]}
 jingle = {git = "https://github.com/toolCHAINZ/jingle.git", branch = "main", features = ["pyo3"]}
 toml_edit = "0.22.22"
+z3 = { git = "https://github.com/toolCHAINZ/z3.rs.git", branch = "patch-1" }
 
 [dev-dependencies]
 pyo3 = { version = "0.24", features = ["extension-module"] }
+z3 = { git = "https://github.com/toolCHAINZ/z3.rs.git", branch = "patch-1" }

crackers_python/build.rs

@@ -0,0 +1,17 @@
+use std::process::Command;
+
+fn main() {
+    // Run the Python script to get the venv's lib directory
+    let output = Command::new("python3")
+        .arg("find_venv_library_path.py")
+        .output()
+        .expect("Failed to execute Python script");
+
+    if !output.status.success() {
+        panic!("cargo:warning=Could not find python's z3, this wheel is unlikely to work.");
+    } else {
+        let venv_lib = String::from_utf8_lossy(&output.stdout).trim().to_string();
+        let z3_python_lib = std::path::Path::new(&venv_lib).join("z3").join("lib");
+        println!("cargo:rustc-link-search=native={}", z3_python_lib.display());
+    }
+}

crackers_python/find_venv_library_path.py

@@ -0,0 +1,9 @@
+import sys
+import os
+import sysconfig
+
+# Get the virtual environment's lib directory
+venv_lib = sysconfig.get_paths()["purelib"]
+
+# Print the path so that we can capture it in build.rs
+print(venv_lib)

crackers_python/src/lib.rs

@@ -14,10 +14,12 @@ use ::crackers::config::synthesis::SynthesisConfig;
 use ::crackers::gadget::library::builder::GadgetLibraryConfig;
 use ::crackers::synthesis::builder::SynthesisSelectionStrategy;
 use pyo3::prelude::*;
+use std::ffi::CString;
 
 /// A Python module implemented in Rust.
 #[pymodule]
 fn crackers(m: &Bound<'_, PyModule>) -> PyResult<()> {
+    m.py().run(&CString::new("import z3")?, None, None)?;
     m.add_class::<PythonCrackersConfig>()?;
     m.add_class::<MetaConfig>()?;
     m.add_class::<SpecificationConfig>()?;