Ablation study variant b

toolCHAINZ · toolCHAINZ · commit 1bb2d0e85ad7 · 2024-12-30T20:12:54.000Z
diff --git a/src/bin/crackers/main.rs b/src/bin/crackers/main.rs
@@ -56,7 +56,6 @@ fn new(path: PathBuf) -> anyhow::Result<()> {
     let config = CrackersConfig {
         meta: Default::default(),
         specification: SpecificationConfig {
-            path: "spec.o".to_string(),
             max_instructions: 1,
         },
         library: Default::default(),
@@ -122,7 +121,7 @@ fn synthesize(config: PathBuf) -> anyhow::Result<()> {
         .init();
     let params = p.resolve()?;
 
-    match params.build_single(&z3) {
+    match params.build_combined(&z3) {
         Ok(mut p) => match p.decide() {
             Ok(res) => match res {
                 DecisionResult::AssignmentFound(a) => {
diff --git a/src/config/mod.rs b/src/config/mod.rs
@@ -38,8 +38,7 @@ impl CrackersConfig {
             b.pointer_invariants(c.get_pointer_constraints().collect());
         }
         b.gadget_library(library)
-            .seed(self.meta.seed)
-            .instructions(self.specification.get_spec(&self.sleigh)?);
+            .seed(self.meta.seed).slots(self.specification.max_instructions);
         b.selection_strategy(self.synthesis.strategy);
         b.candidates_per_slot(self.synthesis.max_candidates_per_slot);
         b.parallel(self.synthesis.parallel).seed(self.meta.seed);
diff --git a/src/config/specification.rs b/src/config/specification.rs
@@ -1,45 +1,10 @@
-use std::fs;
-
-use jingle::sleigh::context::loaded::LoadedSleighContext;
-use jingle::sleigh::Instruction;
-use object::{File, Object, ObjectSymbol};
 use serde::{Deserialize, Serialize};
 
-use crate::config::error::CrackersConfigError;
-use crate::config::error::CrackersConfigError::{SpecMissingStartSymbol, SpecMissingTextSection};
-use crate::config::object::load_sleigh_spec;
-use crate::config::sleigh::SleighConfig;
-
 #[derive(Clone, Debug, Deserialize, Serialize)]
 pub struct SpecificationConfig {
-    pub path: String,
     pub max_instructions: usize,
 }
 
 impl SpecificationConfig {
-    pub fn load_sleigh<'a>(
-        &self,
-        sleigh_config: &'a SleighConfig,
-    ) -> Result<LoadedSleighContext<'a>, CrackersConfigError> {
-        load_sleigh_spec(&self.path, sleigh_config)
-    }
 
-    pub fn get_spec(
-        &self,
-        sleigh_config: &SleighConfig,
-    ) -> Result<Vec<Instruction>, CrackersConfigError> {
-        let data = fs::read(&self.path)?;
-        let gimli_file = File::parse(&*data)?;
-        let sym = gimli_file
-            .symbol_by_name("_start")
-            .ok_or(SpecMissingStartSymbol)?;
-        let _section = gimli_file
-            .section_by_name(".text")
-            .ok_or(SpecMissingTextSection)?;
-        let sleigh = self.load_sleigh(sleigh_config)?;
-        let instrs: Vec<Instruction> = sleigh
-            .read_until_branch(sym.address(), self.max_instructions)
-            .collect();
-        Ok(instrs)
-    }
 }
diff --git a/src/gadget/another_iterator.rs b/src/gadget/another_iterator.rs
@@ -1,12 +1,15 @@
+use std::sync::Arc;
+
 use jingle::modeling::{ModeledInstruction, ModelingContext};
 use jingle::sleigh::{Instruction, OpCode};
 use jingle::JingleContext;
 use tracing::trace;
-use z3::ast::Ast;
+use z3::ast::{Ast, Bool};
 use z3::Solver;
 
 use crate::gadget::signature::GadgetSignature;
 use crate::gadget::Gadget;
+use crate::synthesis::builder::StateConstraintGenerator;
 
 pub struct TraceCandidateIterator<'ctx, 'a, T>
 where
@@ -15,20 +18,27 @@ where
     jingle: JingleContext<'ctx>,
     _solver: Solver<'ctx>,
     gadgets: T,
-    trace: Vec<ModeledInstruction<'ctx>>,
+    step_length: usize,
+    postconditions: Vec<Arc<StateConstraintGenerator>>,
 }
 
 impl<'ctx, 'a, T> TraceCandidateIterator<'ctx, 'a, T>
 where
     T: Iterator<Item = &'a Gadget>,
 {
-    pub(crate) fn new(jingle: &JingleContext<'ctx>, gadgets: T, trace: Vec<ModeledInstruction<'ctx>>) -> Self {
+    pub(crate) fn new(
+        jingle: &JingleContext<'ctx>,
+        gadgets: T,
+        step_length: usize,
+        postconditions: Vec<Arc<StateConstraintGenerator>>,
+    ) -> Self {
         let _solver = Solver::new(jingle.z3);
         Self {
             jingle: jingle.clone(),
             _solver,
             gadgets,
-            trace,
+            step_length,
+            postconditions,
         }
     }
 }
@@ -39,41 +49,27 @@ where
     type Item = Vec<Option<&'a Gadget>>;
 
     fn next(&mut self) -> Option<Self::Item> {
-        let mut next_entry = vec![None; self.trace.len()];
         loop {
             let gadget = self.gadgets.next()?;
-            let gadget_signature = GadgetSignature::from(gadget);
             trace!("Evaluating gadget at {:x}", gadget.address());
-            let is_candidate: Vec<bool> = self
-                .trace
-                .iter()
-                .map(|i| {
-                    trace!("Checking {} signature vs gadget {}", i.instr.disassembly, gadget);
-
-                    gadget_signature.covers(&GadgetSignature::from_instr(&i.instr, i))
-                        && has_compatible_control_flow(&i.instr, gadget)
-                })
-                .collect();
-            if is_candidate.iter().any(|b| *b) {
-                let model = gadget.model(&self.jingle);
-                if let Ok(model) = &model {
-                    is_candidate.iter().enumerate().for_each(|(i, c)| {
-                        if *c {
-                            let expr = model
-                                .upholds_postcondition(&self.trace[i])
-                                .unwrap()
-                                .simplify();
-                            if !expr.is_const() || expr.as_bool().unwrap() {
-                                next_entry[i] = Some(gadget)
+            let model = gadget.model(&self.jingle);
+            if let Ok(model) = &model {
+                for predicate in &self.postconditions {
+                    let f = predicate(&self.jingle, model.get_final_state(), 0);
+                    let i = predicate(&self.jingle, model.get_original_state(), 0);
+                    if let Ok(f) = f{
+                        if let Ok(i) = i {
+                            let f = f.simplify();
+                            //
+                            if f.is_const() && f.as_bool().unwrap() || !f.is_const(){
+                                let i = i.simplify();
+                                if !f._eq(&i).simplify().is_const(){
+                                    return Some(vec![Some(gadget); self.step_length]);
+                                }
                             }
                         }
-                    })
-                }else{
-                    trace!("Could not model gadget: \n{}", gadget)
+                    }
                 }
-                return Some(next_entry);
-            } else {
-                continue;
             }
         }
     }
diff --git a/src/gadget/library/mod.rs b/src/gadget/library/mod.rs
@@ -1,17 +1,18 @@
-use std::collections::HashMap;
-
 use jingle::modeling::ModeledInstruction;
 use jingle::sleigh::context::loaded::LoadedSleighContext;
 use jingle::sleigh::{Instruction, RegisterManager, SpaceInfo, SpaceManager, VarNode};
 use jingle::{JingleContext, JingleError};
 use rand::rngs::StdRng;
 use rand::seq::SliceRandom;
 use rand::SeedableRng;
+use std::collections::HashMap;
+use std::sync::Arc;
 use tracing::{event, Level};
 
 use crate::gadget::another_iterator::TraceCandidateIterator;
 use crate::gadget::library::builder::GadgetLibraryParams;
 use crate::gadget::Gadget;
+use crate::synthesis::builder::StateConstraintGenerator;
 
 pub mod builder;
 pub mod image;
@@ -33,12 +34,13 @@ impl GadgetLibrary {
     pub fn get_random_candidates_for_trace<'ctx, 'a: 'ctx>(
         &'a self,
         jingle: &JingleContext<'ctx>,
-        trace: &[ModeledInstruction<'ctx>],
+        trace_length: usize,
+        postconditions: &[Arc<StateConstraintGenerator>],
         seed: i64,
     ) -> impl Iterator<Item = Vec<Option<&'a Gadget>>> + 'ctx {
         let mut rng = StdRng::seed_from_u64(seed as u64);
         let r = self.gadgets.choose_multiple(&mut rng, self.gadgets.len());
-        TraceCandidateIterator::new(jingle, r, trace.to_vec())
+        TraceCandidateIterator::new(jingle, r, trace_length, postconditions.to_vec())
     }
     pub(super) fn build_from_image(
         sleigh: LoadedSleighContext,
diff --git a/src/synthesis/builder.rs b/src/synthesis/builder.rs
@@ -2,7 +2,6 @@ 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;
@@ -44,7 +43,7 @@ pub struct SynthesisParams {
     pub gadget_library: Arc<GadgetLibrary>,
     pub candidates_per_slot: usize,
     pub parallel: usize,
-    pub instructions: Vec<Instruction>,
+    pub slots: usize,
     #[builder(default)]
     pub preconditions: Vec<Arc<StateConstraintGenerator>>,
     #[builder(default)]
diff --git a/src/synthesis/combined.rs b/src/synthesis/combined.rs
@@ -15,28 +15,14 @@ pub struct CombinedAssignmentSynthesis<'a> {
 
 impl<'a> CombinedAssignmentSynthesis<'a> {
     pub fn decide(&mut self) -> Result<DecisionResult<'a, ModeledBlock<'a>>, CrackersError> {
-        let mut ordering: Vec<Vec<Instruction>> = self
-            .base_config
-            .instructions
-            .partitions()
-            .map(|part| {
-                part.into_iter()
-                    .map(|instrs| Instruction::try_from(instrs).unwrap())
-                    .collect::<Vec<Instruction>>()
-            })
-            .collect();
-        // let mut blacklist = HashSet::new();
-        // todo: gross hack to avoid rewriting the partitioning algorithm to be breadth-first
-        ordering.sort_by(|a, b| a.len().partial_cmp(&b.len()).unwrap());
-        let iter = ordering.into_iter();
         let mut last: Option<DecisionResult<'a, ModeledBlock<'a>>> = None;
-        for instructions in iter {
+        for i in 1..=self.base_config.slots{
             // todo: filter for instruction combinations that have already been ruled out?
             // if instructions.iter().any(|i| blacklist.contains(i)) {
             //     continue;
             // }
             let mut new_config = self.base_config.clone();
-            new_config.instructions = instructions;
+            new_config.slots = i;
             let synth = AssignmentSynthesis::new(self.z3, &new_config);
             if let Ok(mut synth) = synth {
                 // this one constructed, let's try it
diff --git a/src/synthesis/mod.rs b/src/synthesis/mod.rs
@@ -59,29 +59,20 @@ pub struct AssignmentSynthesis<'ctx> {
     preconditions: Vec<Arc<StateConstraintGenerator>>,
     postconditions: Vec<Arc<StateConstraintGenerator>>,
     candidates_per_slot: usize,
-    instructions: Vec<Instruction>,
+    slots: usize,
     parallel: usize,
 }
 
 impl<'ctx> AssignmentSynthesis<'ctx> {
     pub fn new(z3: &'ctx Context, builder: &SynthesisParams) -> Result<Self, CrackersError> {
-        let instrs = &builder.instructions;
-        if instrs.is_empty() {
-            return Err(EmptySpecification);
-        }
         let jingle = JingleContext::new(z3, builder.gadget_library.as_ref());
-        let modeled_instrs: Vec<ModeledInstruction<'ctx>> = instrs
-            .iter()
-            .map(|i| {
-                ModeledInstruction::new(i.clone(), &jingle).unwrap()
-            })
-            .collect();
 
         let candidates = CandidateBuilder::default()
             .with_random_sample_size(builder.candidates_per_slot)
             .build(builder.gadget_library.get_random_candidates_for_trace(
                 &jingle,
-                modeled_instrs.as_slice(),
+                builder.slots,
+                builder.postconditions.as_slice(),
                 builder.seed,
             ))?;
         let outer_problem = match builder.selection_strategy {
@@ -92,9 +83,6 @@ impl<'ctx> AssignmentSynthesis<'ctx> {
                 OptimizeProb(OptimizationProblem::initialize(z3, &candidates.candidates))
             }
         };
-        for x in &builder.instructions {
-            println!("{}", x.disassembly)
-        }
         Ok(AssignmentSynthesis {
             z3,
             outer_problem,
@@ -104,7 +92,7 @@ impl<'ctx> AssignmentSynthesis<'ctx> {
             preconditions: builder.preconditions.clone(),
             postconditions: builder.postconditions.clone(),
             candidates_per_slot: builder.candidates_per_slot,
-            instructions: builder.instructions.clone(),
+            slots: builder.slots,
             parallel: builder.parallel,
         })
     }
@@ -117,8 +105,7 @@ impl<'ctx> AssignmentSynthesis<'ctx> {
             .with_pointer_invariants(&self.pointer_invariants)
             .with_preconditions(&self.preconditions)
             .with_postconditions(&self.postconditions)
-            .with_max_candidates(self.candidates_per_slot)
-            .with_templates(self.instructions.clone().into_iter());
+            .with_max_candidates(self.candidates_per_slot);
         let (resp_sender, resp_receiver) = std::sync::mpsc::channel();
         std::thread::scope(|s| {
             for idx in 0..self.parallel {
diff --git a/src/synthesis/pcode_theory/builder.rs b/src/synthesis/pcode_theory/builder.rs
diff --git a/src/synthesis/pcode_theory/mod.rs b/src/synthesis/pcode_theory/mod.rs
diff --git a/src/synthesis/pcode_theory/pcode_assignment.rs b/src/synthesis/pcode_theory/pcode_assignment.rs
diff --git a/src/synthesis/pcode_theory/theory_worker.rs b/src/synthesis/pcode_theory/theory_worker.rs
