More tweaks to use jingle context

toolCHAINZ · toolCHAINZ · commit e9bd38c61d94 · 2024-12-13T11:41:21.000Z
diff --git a/src/config/constraint.rs b/src/config/constraint.rs
@@ -1,16 +1,14 @@
-use std::collections::HashMap;
-use std::sync::Arc;
-
+use crate::error::CrackersError;
+use crate::synthesis::builder::{StateConstraintGenerator, TransitionConstraintGenerator};
 use jingle::modeling::{ModeledBlock, ModelingContext, State};
 use jingle::sleigh::{IndirectVarNode, RegisterManager, SpaceManager, VarNode};
 use jingle::varnode::{ResolvedIndirectVarNode, ResolvedVarnode};
+use jingle::JingleContext;
 use serde::{Deserialize, Serialize};
+use std::collections::HashMap;
+use std::sync::Arc;
 use tracing::{event, Level};
 use z3::ast::{Ast, Bool, BV};
-use z3::Context;
-
-use crate::error::CrackersError;
-use crate::synthesis::builder::{StateConstraintGenerator, TransitionConstraintGenerator};
 
 #[derive(Clone, Debug, Deserialize, Serialize)]
 pub struct Constraint {
@@ -122,14 +120,14 @@ pub struct PointerRange {
 /// Generates a state constraint that a given varnode must be equal to a given value
 pub fn gen_memory_constraint(
     m: MemoryEqualityConstraint,
-) -> impl for<'a, 'b> Fn(&'a Context, &'b State<'a>, u64) -> Result<Bool<'a>, CrackersError>
+) -> impl for<'a,> Fn(&JingleContext<'a>, &State<'a>, u64) -> Result<Bool<'a>, CrackersError>
        + Send
        + Sync
        + Clone
        + 'static {
-    return move |z3, state, _addr| {
+    return move |jingle, state, _addr| {
         let data = state.read_varnode(&state.varnode(&m.space, m.address, m.size).unwrap())?;
-        let constraint = data._eq(&BV::from_u64(z3, m.value as u64, data.get_size()));
+        let constraint = data._eq(&BV::from_u64(jingle.z3, m.value as u64, data.get_size()));
         Ok(constraint)
     };
 }
@@ -139,14 +137,14 @@ pub fn gen_memory_constraint(
 pub fn gen_register_constraint(
     vn: VarNode,
     value: u64,
-) -> impl for<'a, 'b> Fn(&'a Context, &'b State<'a>, u64) -> Result<Bool<'a>, CrackersError>
+) -> impl for<'a> Fn(&JingleContext<'a>, &State<'a>, u64) -> Result<Bool<'a>, CrackersError>
        + 'static
        + Send
        + Sync
        + Clone {
-    return move |z3, state, _addr| {
+    return move |jingle, state, _addr| {
         let data = state.read_varnode(&vn)?;
-        let constraint = data._eq(&BV::from_u64(z3, value, data.get_size()));
+        let constraint = data._eq(&BV::from_u64(jingle.z3, value, data.get_size()));
         Ok(constraint)
     };
 }
@@ -157,14 +155,14 @@ pub fn gen_register_pointer_constraint<'ctx>(
     vn: VarNode,
     value: String,
     m: Option<PointerRangeConstraints>,
-) -> impl for<'a, 'b> Fn(&'a Context, &'b State<'a>, u64) -> Result<Bool<'a>, CrackersError> + 'ctx + Clone
+) -> impl for<'a> Fn(&JingleContext<'a>, &State<'a>, u64) -> Result<Bool<'a>, CrackersError> + 'ctx + Clone
 {
-    return move |z3, state, _addr| {
+    return move |jingle, state, _addr| {
         let m = m.clone();
         let val = value
             .as_bytes()
             .iter()
-            .map(|b| BV::from_u64(z3, *b as u64, 8))
+            .map(|b| BV::from_u64(jingle.z3, *b as u64, 8))
             .reduce(|a, b| a.concat(&b))
             .unwrap();
         let pointer = state.read_varnode(&vn)?;
@@ -182,9 +180,9 @@ pub fn gen_register_pointer_constraint<'ctx>(
         let mut constraint = data._eq(&val);
         if let Some(c) = m.and_then(|m| m.read) {
             let callback = gen_pointer_range_state_invariant(c);
-            let cc = callback(z3, &resolved, state)?;
+            let cc = callback(jingle, &resolved, state)?;
             if let Some(b) = cc {
-                constraint = Bool::and(z3, &[constraint, b])
+                constraint = Bool::and(jingle.z3, &[constraint, b])
             }
         }
         Ok(constraint)
@@ -195,14 +193,14 @@ pub fn gen_register_pointer_constraint<'ctx>(
 /// the given range.
 pub fn gen_pointer_range_state_invariant<'ctx>(
     m: Vec<PointerRange>,
-) -> impl for<'a, 'b> Fn(
-    &'a Context,
-    &'b ResolvedVarnode<'a>,
-    &'b State<'a>,
+) -> impl for<'a> Fn(
+    &JingleContext<'a>,
+    &ResolvedVarnode<'a>,
+    &State<'a>,
 ) -> Result<Option<Bool<'a>>, CrackersError>
        + 'ctx
        + Clone {
-    return move |z3, vn, state| {
+    return move |jingle, vn, state| {
         match vn {
             ResolvedVarnode::Direct(d) => {
                 // todo: this is gross
@@ -213,51 +211,51 @@ pub fn gen_pointer_range_state_invariant<'ctx>(
                         let bool = m
                             .iter()
                             .any(|mm| d.offset >= mm.min && (d.offset + d.size as u64) <= mm.max);
-                        Ok(Some(Bool::from_bool(z3, bool)))
+                        Ok(Some(Bool::from_bool(jingle.z3, bool)))
                     }
                 }
             }
             ResolvedVarnode::Indirect(vn) => {
                 let mut terms = vec![];
                 for mm in &m {
-                    let min = BV::from_u64(z3, mm.min, vn.pointer.get_size());
-                    let max = BV::from_u64(z3, mm.max, vn.pointer.get_size());
+                    let min = BV::from_u64(jingle.z3, mm.min, vn.pointer.get_size());
+                    let max = BV::from_u64(jingle.z3, mm.max, vn.pointer.get_size());
                     let constraint =
-                        Bool::and(z3, &[vn.pointer.bvuge(&min), vn.pointer.bvule(&max)]);
+                        Bool::and(jingle.z3, &[vn.pointer.bvuge(&min), vn.pointer.bvule(&max)]);
                     terms.push(constraint);
                 }
 
-                Ok(Some(Bool::or(z3, terms.as_slice())))
+                Ok(Some(Bool::or(jingle.z3, terms.as_slice())))
             }
         }
     };
 }
 
 pub fn gen_pointer_range_transition_invariant(
     m: PointerRangeConstraints,
-) -> impl for<'a, 'b> Fn(&'a Context, &'b ModeledBlock<'a>) -> Result<Option<Bool<'a>>, CrackersError>
+) -> impl for<'a> Fn(&JingleContext<'a>, &ModeledBlock<'a>) -> Result<Option<Bool<'a>>, CrackersError>
        + Send
        + Sync
        + Clone
        + 'static {
-    return move |z3, block| {
+    return move |jingle, block| {
         let mut bools = vec![];
         if let Some(r) = &m.read {
             let inv = gen_pointer_range_state_invariant(r.clone());
             for x in block.get_inputs() {
-                if let Some(c) = inv(z3, &x, block.get_final_state())? {
+                if let Some(c) = inv(jingle, &x, block.get_final_state())? {
                     bools.push(c);
                 }
             }
         }
         if let Some(r) = &m.write {
             let inv = gen_pointer_range_state_invariant(r.clone());
             for x in block.get_outputs() {
-                if let Some(c) = inv(z3, &x, block.get_final_state())? {
+                if let Some(c) = inv(jingle, &x, block.get_final_state())? {
                     bools.push(c);
                 }
             }
         }
-        Ok(Some(Bool::and(z3, &bools)))
+        Ok(Some(Bool::and(jingle.z3, &bools)))
     };
 }
diff --git a/src/synthesis/builder.rs b/src/synthesis/builder.rs
@@ -3,6 +3,7 @@ use std::sync::Arc;
 use derive_builder::Builder;
 use jingle::modeling::{ModeledBlock, State};
 use jingle::sleigh::Instruction;
+use jingle::JingleContext;
 use serde::{Deserialize, Serialize};
 use z3::ast::Bool;
 use z3::Context;
@@ -21,11 +22,11 @@ pub enum SynthesisSelectionStrategy {
     OptimizeStrategy,
 }
 
-pub type StateConstraintGenerator = dyn for<'a, 'b> Fn(&'a Context, &'b State<'a>, u64) -> Result<Bool<'a>, CrackersError>
+pub type StateConstraintGenerator = dyn for<'a> Fn(&JingleContext<'a>, &State<'a>, u64) -> Result<Bool<'a>, CrackersError>
     + Send
     + Sync
     + 'static;
-pub type TransitionConstraintGenerator = dyn for<'a, 'b> Fn(&'a Context, &'b ModeledBlock<'a>) -> Result<Option<Bool<'a>>, CrackersError>
+pub type TransitionConstraintGenerator = dyn for<'a> Fn(&JingleContext<'a>, &ModeledBlock<'a>) -> Result<Option<Bool<'a>>, CrackersError>
     + Send
     + Sync
     + 'static;
diff --git a/src/synthesis/mod.rs b/src/synthesis/mod.rs
@@ -140,11 +140,11 @@ impl<'ctx> AssignmentSynthesis<'ctx> {
                         let worker = TheoryWorker::new(&z3, idx, r, req_receiver, t).unwrap();
                         event!(Level::TRACE, "Created worker {}", idx);
                         worker.run();
-                        std::mem::drop(worker);
+                        drop(worker);
                     });
                 });
             }
-            std::mem::drop(resp_sender);
+            drop(resp_sender);
             for (i, x) in req_channels.iter().enumerate() {
                 event!(
                     Level::TRACE,
@@ -185,7 +185,7 @@ impl<'ctx> AssignmentSynthesis<'ctx> {
                                     "Theory returned SAT for {:?}!",
                                     response.assignment
                                 );
-                                dbg!("huh");
+                                dbg!("Terminating remaining workers");
                                 req_channels.clear();
                                 for x in &kill_senders {
                                     x.send(()).unwrap();
@@ -195,10 +195,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!("huh2");
+                                dbg!("Workers Terminated; building and checking model");
                                 let solver = Solver::new(self.z3);
-                                let model = a.check(self.z3, &solver)?;
-                                dbg!("here");
+                                let jingle = JingleContext::new(self.z3, self.library.as_ref());
+                                let model = a.check(&jingle, &solver)?;
+                                dbg!("Model built");
                                 return Ok(DecisionResult::AssignmentFound(model));
                             }
                             Some(c) => {
diff --git a/src/synthesis/pcode_theory/mod.rs b/src/synthesis/pcode_theory/mod.rs
@@ -121,7 +121,7 @@ impl<'ctx, S: ModelingContext<'ctx>> PcodeTheory<'ctx, S> {
         for (index, (spec, g)) in self.templates.iter().zip(&gadgets).enumerate() {
             let sem = Bool::fresh_const(self.j.z3, "c");
             self.solver.assert_and_track(
-                &assert_compatible_semantics(self.j.z3, spec, g, &self.pointer_invariants)?,
+                &assert_compatible_semantics(&self.j, spec, g, &self.pointer_invariants)?,
                 &sem,
             );
             assertions.push(ConjunctiveConstraint::new(
@@ -165,15 +165,15 @@ impl<'ctx, S: ModelingContext<'ctx>> PcodeTheory<'ctx, S> {
         state: &State<'ctx>,
         addr: u64,
     ) -> Result<Bool<'ctx>, CrackersError> {
-        assert_state_constraints(self.j.z3, &self.preconditions, state, addr)
+        assert_state_constraints(&self.j, &self.preconditions, state, addr)
     }
 
     fn assert_postconditions(
         &self,
         state: &State<'ctx>,
         addr: u64,
     ) -> Result<Bool<'ctx>, CrackersError> {
-        assert_state_constraints(self.j.z3, &self.postconditions, state, addr)
+        assert_state_constraints(&self.j, &self.postconditions, state, addr)
     }
 
     fn collect_conflicts(
diff --git a/src/synthesis/pcode_theory/pcode_assignment.rs b/src/synthesis/pcode_theory/pcode_assignment.rs
@@ -1,6 +1,6 @@
-use std::sync::Arc;
-
 use jingle::modeling::{ModeledBlock, ModeledInstruction, ModelingContext, State};
+use jingle::JingleContext;
+use std::sync::Arc;
 use z3::ast::Bool;
 use z3::{Context, SatResult, Solver};
 
@@ -35,30 +35,30 @@ impl<'ctx> PcodeAssignment<'ctx> {
 
     pub fn check(
         &self,
-        z3: &'ctx Context,
+        jingle: &JingleContext<'ctx>,
         solver: &Solver<'ctx>,
     ) -> Result<AssignmentModel<'ctx, ModeledBlock<'ctx>>, CrackersError> {
-        solver.assert(&assert_concat(z3, &self.spec_trace)?);
+        solver.assert(&assert_concat(jingle.z3, &self.spec_trace)?);
         for x in self.eval_trace.windows(2) {
             solver.assert(&x[0].assert_concat(&x[1])?);
             solver.assert(&x[0].can_branch_to_address(x[1].get_address())?);
         }
         for (spec_inst, trace_inst) in self.spec_trace.iter().zip(&self.eval_trace) {
             solver.assert(&assert_compatible_semantics(
-                z3,
+                jingle,
                 spec_inst,
                 trace_inst,
                 &self.pointer_invariants,
             )?);
         }
         solver.assert(&assert_state_constraints(
-            z3,
+            jingle,
             &self.preconditions,
             self.eval_trace.as_slice().get_original_state(),
             self.eval_trace[0].get_first_address(),
         )?);
         solver.assert(&assert_state_constraints(
-            z3,
+            jingle,
             &self.postconditions,
             self.eval_trace.as_slice().get_final_state(),
             self.eval_trace.last().unwrap().get_last_address(),
@@ -86,7 +86,7 @@ pub fn assert_concat<'ctx, T: ModelingContext<'ctx>>(
 }
 
 pub fn assert_compatible_semantics<'ctx, S: ModelingContext<'ctx>>(
-    z3: &'ctx Context,
+    jingle: &JingleContext<'ctx>,
     spec: &S,
     item: &ModeledBlock<'ctx>,
     invariants: &[Arc<TransitionConstraintGenerator>],
@@ -102,24 +102,24 @@ pub fn assert_compatible_semantics<'ctx, S: ModelingContext<'ctx>>(
     }
     // Thirdly, every input and output address must pass our pointer constraints
     for invariant in invariants.iter() {
-        let inv = invariant(z3, item)?;
+        let inv = invariant(jingle, item)?;
         if let Some(b) = inv {
             bools.push(b)
         }
     }
-    Ok(Bool::and(z3, &bools))
+    Ok(Bool::and(jingle.z3, &bools))
 }
 
 pub fn assert_state_constraints<'ctx>(
-    z3: &'ctx Context,
+    jingle: &JingleContext<'ctx>,
     constraints: &[Arc<StateConstraintGenerator>],
     state: &State<'ctx>,
     addr: u64,
 ) -> Result<Bool<'ctx>, CrackersError> {
     let mut bools = vec![];
     for x in constraints.iter() {
-        let assertion = x(z3, state, addr)?;
+        let assertion = x(jingle, state, addr)?;
         bools.push(assertion);
     }
-    Ok(Bool::and(z3, &bools))
+    Ok(Bool::and(jingle.z3, &bools))
 }
