Skip to content

Commit

Permalink
make more things owned
Browse files Browse the repository at this point in the history
  • Loading branch information
@ekiwi
ekiwi committed Apr 16, 2024
1 parent 9c03d8b commit 9eb48bb
Show file tree
Hide file tree
Showing 5 changed files with 45 additions and 34 deletions.
21 changes: 13 additions & 8 deletions synth/src/basic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,15 +36,15 @@ pub fn generate_minimal_repair<S: Simulator, E: TransitionSystemEncoding>(
let end_step = end_step_option.unwrap_or(rctx.tb.step_count() - 1);

// start encoding
rctx.enc.init_at(rctx.ctx, rctx.smt_ctx, start_step)?;
rctx.enc.init_at(rctx.ctx, &mut rctx.smt_ctx, start_step)?;

// constrain starting state to that from the simulator
constrain_starting_state(rctx, start_step)?;

let start_unroll = std::time::Instant::now();
// unroll system and constrain inputs and outputs
for _ in start_step..end_step {
rctx.enc.unroll(rctx.ctx, rctx.smt_ctx)?;
rctx.enc.unroll(rctx.ctx, &mut rctx.smt_ctx)?;
}
if rctx.verbose {
println!(
Expand All @@ -54,8 +54,13 @@ pub fn generate_minimal_repair<S: Simulator, E: TransitionSystemEncoding>(
}

let start_apply_const = std::time::Instant::now();
rctx.tb
.apply_constraints(rctx.ctx, rctx.smt_ctx, rctx.enc, start_step, end_step)?;
rctx.tb.apply_constraints(
rctx.ctx,
&mut rctx.smt_ctx,
&mut rctx.enc,
start_step,
end_step,
)?;
if rctx.verbose {
println!(
"Took {:?} to apply constraints",
Expand Down Expand Up @@ -84,9 +89,9 @@ pub fn generate_minimal_repair<S: Simulator, E: TransitionSystemEncoding>(
println!("Found a minimal solution with {min_num_changes} changes.")
}

let solution = rctx
.synth_vars
.read_assignment(rctx.ctx, rctx.smt_ctx, rctx.enc, start_step);
check_assuming_end(rctx.smt_ctx, &rctx.solver)?;
let solution =
rctx.synth_vars
.read_assignment(rctx.ctx, &mut rctx.smt_ctx, &mut rctx.enc, start_step);
check_assuming_end(&mut rctx.smt_ctx, &rctx.solver)?;
Ok(Some((solution, min_num_changes)))
}
4 changes: 2 additions & 2 deletions synth/src/filters.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,11 @@ pub fn can_be_repaired_from_arbitrary_state<S: Simulator, E: TransitionSystemEnc
rctx.smt_ctx.push_many(1)?;

// start encoding
rctx.enc.init_at(rctx.ctx, rctx.smt_ctx, fail_at)?;
rctx.enc.init_at(rctx.ctx, &mut rctx.smt_ctx, fail_at)?;

// apply output / input constraints
rctx.tb
.apply_constraints(rctx.ctx, rctx.smt_ctx, rctx.enc, fail_at, fail_at)?;
.apply_constraints(rctx.ctx, &mut rctx.smt_ctx, &mut rctx.enc, fail_at, fail_at)?;

// let's seee if a solution exists
let r = rctx.smt_ctx.check()?;
Expand Down
20 changes: 12 additions & 8 deletions synth/src/incremental.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,8 @@ where
start: step_range.start,
stop: StopAt::first_fail_or_step(step_range.end),
};
let res = self.rctx.tb.run(self.rctx.sim, &conf, self.verbose());
let verbose = self.verbose();
let res = self.rctx.tb.run(&mut self.rctx.sim, &conf, verbose);
assert_eq!(res.first_fail_at, Some(self.conf.fail_at), "{conf:?}");

// start new SMT context to make it easy to later revert everything
Expand Down Expand Up @@ -122,16 +123,16 @@ where
// try to find a different solution
self.rctx.synth_vars.block_assignment(
self.rctx.ctx,
self.rctx.smt_ctx,
self.rctx.enc,
&mut self.rctx.smt_ctx,
&mut self.rctx.enc,
&repair,
step_range.start,
)?;
maybe_repair = match self.rctx.smt_ctx.check()? {
Response::Sat => Some(self.rctx.synth_vars.read_assignment(
self.rctx.ctx,
self.rctx.smt_ctx,
self.rctx.enc,
&mut self.rctx.smt_ctx,
&mut self.rctx.enc,
step_range.start,
)),
Response::Unsat | Response::Unknown => None,
Expand Down Expand Up @@ -179,12 +180,14 @@ where
fn test_repair(&mut self, repair: &RepairAssignment) -> RunResult {
let start_step = 0;
self.update_sim_state_to_step(start_step);
self.rctx.synth_vars.apply_to_sim(self.rctx.sim, repair);
self.rctx
.synth_vars
.apply_to_sim(&mut self.rctx.sim, repair);
let conf = RunConfig {
start: start_step,
stop: StopAt::first_fail(),
};
self.rctx.tb.run(self.rctx.sim, &conf, false)
self.rctx.tb.run(&mut self.rctx.sim, &conf, false)
}

fn constrain_changes(&mut self, num_changes: u32, start_step: StepInt) -> Result<()> {
Expand Down Expand Up @@ -214,7 +217,8 @@ where
start: nearest_step,
stop: StopAt::step(step),
};
self.rctx.tb.run(self.rctx.sim, &run_conf, self.verbose());
let verbose = self.verbose();
self.rctx.tb.run(&mut self.rctx.sim, &run_conf, verbose);

// remember the state in case we need to go back
let new_snapshot = self.rctx.sim.take_snapshot();
Expand Down
9 changes: 4 additions & 5 deletions synth/src/main.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -215,18 +215,17 @@ fn main() {
let fail_at = res.first_fail_at.unwrap();

// start solver
let (mut smt_ctx, mut enc) =
start_solver(&args, &mut ctx, &sys).expect("Failed to start SMT solver!");
let (smt_ctx, enc) = start_solver(&args, &mut ctx, &sys).expect("Failed to start SMT solver!");

let mut repair_ctx = RepairContext {
ctx: &mut ctx,
sys: &sys,
sim: &mut sim,
sim,
synth_vars: &synth_vars,
tb: &tb,
change_count_ref,
smt_ctx: &mut smt_ctx,
enc: &mut enc,
smt_ctx,
enc,
solver: args.solver.cmd(),
verbose: args.verbose,
};
Expand Down
25 changes: 14 additions & 11 deletions synth/src/repair.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,12 +29,12 @@ pub struct RepairResult {
pub struct RepairContext<'a, S: Simulator, E: TransitionSystemEncoding> {
pub ctx: &'a mut Context,
pub sys: &'a TransitionSystem,
pub sim: &'a mut S,
pub sim: S,
pub synth_vars: &'a RepairVars,
pub tb: &'a Testbench,
pub change_count_ref: ExprRef,
pub smt_ctx: &'a mut smt::Context,
pub enc: &'a mut E,
pub smt_ctx: smt::Context,
pub enc: E,
pub solver: SmtSolverCmd,
pub verbose: bool,
}
Expand All @@ -45,9 +45,12 @@ pub fn constrain_changes<S: Simulator, E: TransitionSystemEncoding>(
start_step: StepInt,
) -> smt::SExpr {
let change_count_width = rctx.change_count_ref.get_bv_type(rctx.ctx).unwrap();
let change_count_expr =
rctx.enc
.get_at(rctx.ctx, rctx.smt_ctx, rctx.change_count_ref, start_step);
let change_count_expr = rctx.enc.get_at(
rctx.ctx,
&mut rctx.smt_ctx,
rctx.change_count_ref,
start_step,
);
let constraint = rctx.smt_ctx.eq(
change_count_expr,
rctx.smt_ctx
Expand All @@ -63,7 +66,7 @@ pub fn minimize_changes<S: Simulator, E: TransitionSystemEncoding>(
let mut num_changes = 1u32;
loop {
let constraint = constrain_changes(rctx, num_changes, start_step);
match check_assuming(rctx.smt_ctx, constraint, &rctx.solver)? {
match check_assuming(&mut rctx.smt_ctx, constraint, &rctx.solver)? {
smt::Response::Sat => {
// found a solution
return Ok(num_changes);
Expand All @@ -72,7 +75,7 @@ pub fn minimize_changes<S: Simulator, E: TransitionSystemEncoding>(
smt::Response::Unknown => panic!("SMT solver returned unknown!"),
}
// remove assertion for next round
check_assuming_end(rctx.smt_ctx, &rctx.solver)?;
check_assuming_end(&mut rctx.smt_ctx, &rctx.solver)?;
num_changes += 1;
}
}
Expand All @@ -88,18 +91,18 @@ pub fn constrain_starting_state<S: Simulator, E: TransitionSystemEncoding>(
{
let symbol = rctx
.enc
.get_at(rctx.ctx, rctx.smt_ctx, state.symbol, start_step);
.get_at(rctx.ctx, &mut rctx.smt_ctx, state.symbol, start_step);
match state.symbol.get_type(rctx.ctx) {
Type::BV(_) => {
let value = rctx.sim.get(state.symbol).unwrap();
let value_expr = value_to_smt_expr(rctx.smt_ctx, value);
let value_expr = value_to_smt_expr(&mut rctx.smt_ctx, value);
rctx.smt_ctx.assert(rctx.smt_ctx.eq(symbol, value_expr))?;
}
Type::Array(tpe) => {
let elements = 1u64 << tpe.index_width;
for index in 0..elements {
let value = rctx.sim.get_element(state.symbol, index).unwrap();
let value_expr = value_to_smt_expr(rctx.smt_ctx, value);
let value_expr = value_to_smt_expr(&mut rctx.smt_ctx, value);
let index_expr = if tpe.index_width == 1 {
if index == 0 {
rctx.smt_ctx.false_()
Expand Down

0 comments on commit 9eb48bb

Please sign in to comment.