Oh god

Author: toolCHAINZ

jingle/src/modeling/state/space.rs

@@ -25,7 +25,10 @@ impl<'ctx> ModeledSpace<'ctx> {
     /// Create a new modeling space with the given z3 context, using the provided space metadata
     pub(crate) fn new(jingle: &JingleContext<'ctx>, space_info: &SpaceInfo) -> Self {
         let domain = Sort::bitvector(jingle.z3, space_info.index_size_bytes * 8);
+        dbg!(&domain);
         let range = Sort::bitvector(jingle.z3, space_info.word_size_bytes * 8);
+        dbg!(&jingle.z3);
+        dbg!(&range);
         Self {
             endianness: space_info.endianness,
             data: Array::fresh_const(jingle.z3, &space_info.name, &domain, &range),

jingle_python/Cargo.toml

@@ -10,4 +10,9 @@ crate-type = ["cdylib"]
 
 [dependencies]
 pyo3 = "0.24.0"
-jingle = {path = "../jingle", features = ["pyo3", "gimli"]}
+jingle = {path = "../jingle", features = ["pyo3", "gimli"]}
+z3 = { git = "https://github.com/prove-rs/z3.rs.git", branch = "master" }
+z3-sys = { git = "https://github.com/prove-rs/z3.rs.git", branch = "master" }
+
+[build-dependencies]
+pkg-config = "0.3.32"

jingle_python/build.rs

@@ -0,0 +1,13 @@
+
+fn main() {
+    let var = std::env::var("Z3_PYTHON_LIB").unwrap_or_else(|_| "/Users/maroed/RustroverProjects/jingle/jingle_python/.venv/lib/python3.13/site-packages/z3/lib/".to_string());
+    // Get the directory where Python's Z3 library is located
+    let z3_python_lib = std::path::Path::new(&var);
+
+    // Set the environment variable for Rust to use the same library
+    println!("cargo:rerun-if-changed=build.rs");
+    println!("cargo:libdir={}", z3_python_lib.display());
+
+    // Optionally, set the rpath for dynamic libraries
+    println!("cargo:rustc-link-search=native={}", z3_python_lib.display());
+}

jingle_python/pyproject.toml

@@ -12,7 +12,7 @@ classifiers = [
 ]
 dynamic = ["version"]
 dependencies = [
-    "maturin>=1.8.3",
+    "z3-solver==4.12.4.0",
 ]
 [tool.maturin]
 features = ["pyo3/extension-module"]

jingle_python/script.py

@@ -0,0 +1,4 @@
+import z3
+from jingle import *
+sleigh = create_sleigh_context("/Users/maroed/RustroverProjects/code_reuse_synthesis_artifacts/crackers/libz.so.1", "/Applications/ghidra")
+sleigh.make_jingle_context()

jingle_python/src/jingle_context.rs

@@ -0,0 +1,31 @@
+use crate::context_switcheroo;
+use jingle::sleigh::ArchInfoProvider;
+use jingle::JingleContext;
+use pyo3::prelude::*;
+use z3_sys::Z3_context;
+
+#[pyclass(unsendable)]
+pub struct PythonJingleContext {
+    #[allow(unused)]
+    context: JingleContext<'static>,
+}
+
+impl PythonJingleContext {
+    pub fn make_jingle_context<T: ArchInfoProvider>(i: &T) -> PyResult<PythonJingleContext> {
+        Python::with_gil(|py| {
+            let z3_mod = PyModule::import(py, "z3")?;
+            let global_ctx = z3_mod.getattr("main_ctx")?.call0()?;
+            let z3_ptr: usize = global_ctx
+                .getattr("ref")?
+                .call0()?
+                .getattr("value")?
+                .extract()?;
+            println!("z3_ptr: {:x}", z3_ptr);
+            let raw_ctx: Z3_context = z3_ptr as Z3_context;
+            let ctx = context_switcheroo( raw_ctx );
+            let ctx = JingleContext::new(ctx, i);
+            ctx.fresh_state();
+            Ok(PythonJingleContext { context: ctx })
+        })
+    }
+}

jingle_python/src/lib.rs

@@ -1,17 +1,39 @@
-mod sleigh_context;
 mod instruction;
+mod jingle_context;
+mod sleigh_context;
 
-use pyo3::prelude::*;
-use ::jingle::sleigh::{IndirectVarNode, PcodeOperation, VarNode};
-use ::jingle::sleigh::Instruction;
-use sleigh_context::create_sleigh_context;
 use crate::instruction::PythonInstruction;
 use crate::sleigh_context::LoadedSleighContextWrapper;
+use ::jingle::sleigh::{IndirectVarNode, PcodeOperation, VarNode};
+use pyo3::prelude::*;
+use sleigh_context::create_sleigh_context;
+use std::cell::RefCell;
+use std::ffi::CString;
+use std::mem;
+use z3::Context;
+use z3_sys::Z3_context;
 
+thread_local! {
+    pub static CONTEXT: RefCell<Z3_context> = RefCell::new(std::ptr::null_mut());
+}
+
+thread_local! {
+    pub static CTX_REF: &'static Context = CONTEXT.with_borrow(|ctx| unsafe {
+        mem::transmute(ctx)
+    });
+}
+pub fn context_switcheroo(z3: Z3_context) -> &'static Context {
+    CONTEXT.replace(z3);
+    CTX_REF.with(|ctx| {
+        println!("{:p}", *ctx);
+        dbg!(*ctx)
+    })
+}
 
 /// A Python module implemented in Rust.
 #[pymodule]
 fn jingle(m: &Bound<'_, PyModule>) -> PyResult<()> {
+    m.py().run(&CString::new("import z3")?, None, None)?;
     m.add_class::<VarNode>()?;
     m.add_class::<IndirectVarNode>()?;
     m.add_class::<PcodeOperation>()?;
@@ -20,3 +42,19 @@ fn jingle(m: &Bound<'_, PyModule>) -> PyResult<()> {
     m.add_function(wrap_pyfunction!(create_sleigh_context, m)?)?;
     Ok(())
 }
+
+#[cfg(test)]
+mod tests {
+    use crate::sleigh_context::{create_sleigh_context, LoadedSleighContextWrapper};
+
+    #[test]
+    fn ctx() {
+        pyo3::prepare_freethreaded_python();
+        let ctx = create_sleigh_context(
+            "/Users/maroed/RustroverProjects/code_reuse_synthesis_artifacts/crackers/libz.so.1",
+            "/Applications/ghidra",
+        )
+        .unwrap();
+        ctx.make_jingle_context().unwrap();
+    }
+}

jingle_python/src/sleigh_context.rs

@@ -1,9 +1,8 @@
-use std::os::unix::raw::off_t;
 use jingle::sleigh::context::image::gimli::load_with_gimli;
 use jingle::sleigh::context::loaded::LoadedSleighContext;
-use jingle::sleigh::Instruction;
 use pyo3::{pyclass, pyfunction, pymethods, PyResult};
 use crate::instruction::PythonInstruction;
+use crate::jingle_context::PythonJingleContext;
 
 #[pyfunction]
 pub fn create_sleigh_context(
@@ -34,4 +33,8 @@ impl LoadedSleighContextWrapper {
     pub fn get_base_address(&mut self) -> u64 {
         self.context.get_base_address()
     }
+    
+    pub fn make_jingle_context(&self) -> PyResult<PythonJingleContext> {
+        PythonJingleContext::make_jingle_context(&self.context)
+    }
 }