Skip to content

Commit e21da51

Browse files
toolCHAINZtoolCHAINZ
committed
Update for dev branch
1 parent f969608 commit e21da51

File tree

7 files changed

+42
-41
lines changed

7 files changed

+42
-41
lines changed

‎src/gadget/another_iterator.rs‎

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
use jingle::modeling::{ModeledInstruction, ModelingContext};
22
use jingle::sleigh::{Instruction, OpCode};
3-
use tracing::{instrument, trace};
3+
use jingle::JingleContext;
4+
use tracing::trace;
45
use z3::ast::Ast;
5-
use z3::{Context, Solver};
6+
use z3::Solver;
67

78
use crate::gadget::signature::GadgetSignature;
89
use crate::gadget::Gadget;
@@ -11,7 +12,7 @@ pub struct TraceCandidateIterator<'ctx, 'a, T>
1112
where
1213
T: Iterator<Item = &'a Gadget>,
1314
{
14-
z3: &'ctx Context,
15+
jingle: JingleContext<'ctx>,
1516
_solver: Solver<'ctx>,
1617
gadgets: T,
1718
trace: Vec<ModeledInstruction<'ctx>>,
@@ -21,10 +22,10 @@ impl<'ctx, 'a, T> TraceCandidateIterator<'ctx, 'a, T>
2122
where
2223
T: Iterator<Item = &'a Gadget>,
2324
{
24-
pub(crate) fn new(z3: &'ctx Context, gadgets: T, trace: Vec<ModeledInstruction<'ctx>>) -> Self {
25-
let _solver = Solver::new(z3);
25+
pub(crate) fn new(jingle: &JingleContext<'ctx>, gadgets: T, trace: Vec<ModeledInstruction<'ctx>>) -> Self {
26+
let _solver = Solver::new(jingle.z3);
2627
Self {
27-
z3,
28+
jingle: jingle.clone(),
2829
_solver,
2930
gadgets,
3031
trace,
@@ -54,7 +55,7 @@ where
5455
})
5556
.collect();
5657
if is_candidate.iter().any(|b| *b) {
57-
let model = gadget.model(self.z3);
58+
let model = gadget.model(&self.jingle);
5859
if let Ok(model) = &model {
5960
is_candidate.iter().enumerate().for_each(|(i, c)| {
6061
if *c {

‎src/gadget/candidates.rs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
use jingle::modeling::ModeledBlock;
2-
use z3::Context;
2+
use jingle::JingleContext;
33

44
use crate::error::CrackersError;
55
use crate::error::CrackersError::UnsimulatedOperation;
@@ -60,13 +60,13 @@ pub struct Candidates {
6060
impl Candidates {
6161
pub fn model<'ctx>(
6262
&self,
63-
z3: &'ctx Context,
63+
jingle: &JingleContext<'ctx>,
6464
) -> Result<Vec<Vec<ModeledBlock<'ctx>>>, CrackersError> {
6565
let mut result = vec![];
6666
for x in &self.candidates {
6767
let mut v = vec![];
6868
for g in x {
69-
v.push(g.model(z3)?);
69+
v.push(g.model(jingle)?);
7070
}
7171
result.push(v)
7272
}

‎src/gadget/library/mod.rs‎

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,17 @@
11
use std::collections::HashMap;
22

3-
use jingle::JingleError;
43
use jingle::modeling::ModeledInstruction;
5-
use jingle::sleigh::{Instruction, RegisterManager, SpaceInfo, SpaceManager, VarNode};
64
use jingle::sleigh::context::loaded::LoadedSleighContext;
5+
use jingle::sleigh::{Instruction, RegisterManager, SpaceInfo, SpaceManager, VarNode};
6+
use jingle::{JingleContext, JingleError};
77
use rand::rngs::StdRng;
8-
use rand::SeedableRng;
98
use rand::seq::SliceRandom;
9+
use rand::SeedableRng;
1010
use tracing::{event, Level};
11-
use z3::Context;
1211

1312
use crate::gadget::another_iterator::TraceCandidateIterator;
14-
use crate::gadget::Gadget;
1513
use crate::gadget::library::builder::GadgetLibraryParams;
14+
use crate::gadget::Gadget;
1615

1716
pub mod builder;
1817

@@ -32,13 +31,13 @@ impl GadgetLibrary {
3231

3332
pub fn get_random_candidates_for_trace<'ctx, 'a: 'ctx>(
3433
&'a self,
35-
z3: &'ctx Context,
34+
jingle: &JingleContext<'ctx>,
3635
trace: &[ModeledInstruction<'ctx>],
3736
seed: i64,
3837
) -> impl Iterator<Item = Vec<Option<&'a Gadget>>> + 'ctx {
3938
let mut rng = StdRng::seed_from_u64(seed as u64);
4039
let r = self.gadgets.choose_multiple(&mut rng, self.gadgets.len());
41-
TraceCandidateIterator::new(z3, r, trace.to_vec())
40+
TraceCandidateIterator::new(jingle, r, trace.to_vec())
4241
}
4342
pub(super) fn build_from_image(
4443
sleigh: LoadedSleighContext,
@@ -119,8 +118,8 @@ mod tests {
119118
use std::fs;
120119
use std::path::Path;
121120

122-
use elf::ElfBytes;
123121
use elf::endian::AnyEndian;
122+
use elf::ElfBytes;
124123
use jingle::sleigh::context::SleighContextBuilder;
125124

126125
use crate::gadget::library::builder::GadgetLibraryParams;

‎src/gadget/mod.rs‎

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,9 @@
1-
use std::collections::HashSet;
2-
use std::fmt::{Debug, Display, Formatter};
3-
41
use jingle::modeling::ModeledBlock;
52
use jingle::sleigh::{Instruction, OpCode, PcodeOperation, SpaceInfo, SpaceManager};
3+
use jingle::JingleContext;
64
use serde::{Deserialize, Serialize};
7-
use z3::Context;
5+
use std::collections::HashSet;
6+
use std::fmt::{Debug, Display, Formatter};
87

98
use crate::error::CrackersError;
109

@@ -50,8 +49,8 @@ impl Gadget {
5049
.any(|i| i.ops.iter().any(|o| blacklist.contains(&o.opcode())))
5150
}
5251

53-
pub fn model<'ctx>(&self, z3: &'ctx Context) -> Result<ModeledBlock<'ctx>, CrackersError> {
54-
let blk = ModeledBlock::read(z3, self, self.instructions.clone().into_iter())?;
52+
pub fn model<'ctx>(&self, jingle: &JingleContext<'ctx>) -> Result<ModeledBlock<'ctx>, CrackersError> {
53+
let blk = ModeledBlock::read(jingle, self.instructions.clone().into_iter())?;
5554
Ok(blk)
5655
}
5756
}

‎src/synthesis/mod.rs‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
use std::cmp::Ordering;
2-
use std::sync::Arc;
3-
41
use jingle::modeling::{ModeledBlock, ModeledInstruction, ModelingContext};
52
use jingle::sleigh::Instruction;
3+
use jingle::JingleContext;
4+
use std::cmp::Ordering;
5+
use std::sync::Arc;
66
use tracing::{event, instrument, Level};
77
use z3::{Config, Context, Solver};
88

@@ -69,17 +69,18 @@ impl<'ctx> AssignmentSynthesis<'ctx> {
6969
if instrs.is_empty() {
7070
return Err(EmptySpecification);
7171
}
72+
let jingle = JingleContext::new(z3, builder.gadget_library.as_ref());
7273
let modeled_instrs: Vec<ModeledInstruction<'ctx>> = instrs
7374
.iter()
7475
.map(|i| {
75-
ModeledInstruction::new(i.clone(), builder.gadget_library.as_ref(), z3).unwrap()
76+
ModeledInstruction::new(i.clone(), &jingle).unwrap()
7677
})
7778
.collect();
7879

7980
let candidates = CandidateBuilder::default()
8081
.with_random_sample_size(builder.candidates_per_slot)
8182
.build(builder.gadget_library.get_random_candidates_for_trace(
82-
z3,
83+
&jingle,
8384
modeled_instrs.as_slice(),
8485
builder.seed,
8586
))?;
@@ -191,8 +192,9 @@ impl<'ctx> AssignmentSynthesis<'ctx> {
191192
}
192193
kill_senders.clear();
193194
let t = theory_builder.clone();
195+
let jingle = JingleContext::new(self.z3, self.library.as_ref());
194196
let a: PcodeAssignment<'ctx> =
195-
t.build_assignment(self.z3, response.assignment)?;
197+
t.build_assignment(&jingle, response.assignment)?;
196198
dbg!("huh2");
197199
let solver = Solver::new(self.z3);
198200
let model = a.check(self.z3, &solver)?;

‎src/synthesis/pcode_theory/builder.rs‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ pub struct PcodeTheoryBuilder<'lib> {
2626

2727
impl<'lib> PcodeTheoryBuilder<'lib> {
2828
// todo: this is gross
29-
pub fn new(candidates: Candidates, library: &'lib GadgetLibrary) -> PcodeTheoryBuilder {
29+
pub fn new(candidates: Candidates, library: &'lib GadgetLibrary) -> PcodeTheoryBuilder<'lib> {
3030
Self {
3131
templates: Default::default(),
3232
library,
@@ -38,11 +38,11 @@ impl<'lib> PcodeTheoryBuilder<'lib> {
3838
}
3939
}
4040
pub fn build(self, z3: &Context) -> Result<PcodeTheory<ModeledInstruction>, CrackersError> {
41-
let modeled_templates = self.model_instructions(z3)?;
42-
let gadget_candidates = self.candidates.model(z3)?;
43-
let j = JingleContext::new(z3, self.library);
41+
let jingle = JingleContext::new(z3, self.library);
42+
let modeled_templates = self.model_instructions(&jingle)?;
43+
let gadget_candidates = self.candidates.model(&jingle)?;
4444
let t = PcodeTheory::new(
45-
j,
45+
jingle,
4646
modeled_templates,
4747
gadget_candidates,
4848
self.preconditions,
@@ -54,11 +54,11 @@ impl<'lib> PcodeTheoryBuilder<'lib> {
5454

5555
pub fn build_assignment<'ctx>(
5656
&self,
57-
z3: &'ctx Context,
57+
jingle: &JingleContext<'ctx>,
5858
slot_assignments: SlotAssignments,
5959
) -> Result<PcodeAssignment<'ctx>, CrackersError> {
60-
let modeled_templates: Vec<ModeledInstruction<'ctx>> = self.model_instructions(z3)?;
61-
let gadget_candidates: Vec<Vec<ModeledBlock<'ctx>>> = self.candidates.model(z3)?;
60+
let modeled_templates: Vec<ModeledInstruction<'ctx>> = self.model_instructions(jingle)?;
61+
let gadget_candidates: Vec<Vec<ModeledBlock<'ctx>>> = self.candidates.model(jingle)?;
6262
let selected_candidates: Vec<ModeledBlock<'ctx>> = slot_assignments
6363
.choices()
6464
.iter()
@@ -104,11 +104,11 @@ impl<'lib> PcodeTheoryBuilder<'lib> {
104104

105105
fn model_instructions<'ctx>(
106106
&self,
107-
z3: &'ctx Context,
107+
jingle: &JingleContext<'ctx>,
108108
) -> Result<Vec<ModeledInstruction<'ctx>>, CrackersError> {
109109
let mut modeled_templates = vec![];
110110
for template in &self.templates {
111-
modeled_templates.push(ModeledInstruction::new(template.clone(), self.library, z3)?);
111+
modeled_templates.push(ModeledInstruction::new(template.clone(), jingle)?);
112112
}
113113
Ok(modeled_templates)
114114
}

‎src/synthesis/slot_assignments/mod.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ impl SlotAssignments {
6262
pub(crate) fn display_conflict<'a>(
6363
&'a self,
6464
conflicts: &'a ConflictClause,
65-
) -> SlotAssignmentConflictDisplay {
65+
) -> SlotAssignmentConflictDisplay<'a> {
6666
SlotAssignmentConflictDisplay {
6767
assignment: self,
6868
conflict: conflicts,

0 commit comments

Comments
 (0)