Merge remote-tracking branch 'origin/main'

Author: toolCHAINZ

src/synthesis/assignment_model.rs

@@ -1,7 +1,7 @@
 use std::fmt::{Display, Formatter};
 
 use jingle::modeling::{ModelingContext, State};
-use jingle::sleigh::GeneralizedVarNode;
+use jingle::sleigh::{GeneralizedVarNode, RegisterManager};
 use jingle::varnode::ResolvedVarnode;
 use z3::ast::BV;
 use z3::Model;
@@ -40,6 +40,22 @@ impl<'ctx, T: ModelingContext<'ctx>> AssignmentModel<'ctx, T> {
     pub fn read_resolved(&'ctx self, vn: &ResolvedVarnode<'ctx>) -> Option<BV<'ctx>> {
         self.final_state().and_then(|f| f.read_resolved(vn).ok())
     }
+
+    pub fn print_trace_of_reg(&'ctx self, reg: &str) {
+        let r = self.final_state().unwrap().get_register(reg).unwrap();
+        for gadget in &self.gadgets {
+            let val = gadget.get_original_state().read_varnode(&r).unwrap();
+            println!("{} Before: {:?}",reg, self.model.eval(&val, false));
+            let val = gadget.get_final_state().read_varnode(&r).unwrap();
+            println!("{} After: {:?}",reg,  self.model.eval(&val, false));
+        }
+    }
+
+    pub fn initial_reg(&'ctx self, reg: &str) -> Option<BV<'ctx>> {
+        let r = self.final_state().unwrap().get_register(reg).unwrap();
+            let val = self.gadgets[0].get_original_state().read_varnode(&r).unwrap();
+            self.model.eval(&val, false)
+    }
 }
 
 impl<'ctx, T: ModelingContext<'ctx> + Display> Display for AssignmentModel<'ctx, T> {

src/synthesis/builder.rs

@@ -45,8 +45,11 @@ pub struct SynthesisParams {
     pub candidates_per_slot: usize,
     pub parallel: usize,
     pub instructions: Vec<Instruction>,
+    #[builder(default)]
     pub preconditions: Vec<Arc<StateConstraintGenerator>>,
+    #[builder(default)]
     pub postconditions: Vec<Arc<StateConstraintGenerator>>,
+    #[builder(default)]
     pub pointer_invariants: Vec<Arc<TransitionConstraintGenerator>>,
 }
 

src/synthesis/pcode_theory/pcode_assignment.rs

@@ -39,8 +39,8 @@ impl<'ctx> PcodeAssignment<'ctx> {
         solver: &Solver<'ctx>,
     ) -> Result<AssignmentModel<'ctx, ModeledBlock<'ctx>>, CrackersError> {
         solver.assert(&assert_concat(jingle.z3, &self.spec_trace)?);
+        solver.assert(&assert_concat(jingle.z3, &self.eval_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) {