From 9eb48bb20928d134ffbabb74469e355f9f19fe08 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Tue, 16 Apr 2024 12:23:24 -0400 Subject: [PATCH] make more things owned --- synth/src/basic.rs | 21 +++++++++++++-------- synth/src/filters.rs | 4 ++-- synth/src/incremental.rs | 20 ++++++++++++-------- synth/src/main.rs | 9 ++++----- synth/src/repair.rs | 25 ++++++++++++++----------- 5 files changed, 45 insertions(+), 34 deletions(-) diff --git a/synth/src/basic.rs b/synth/src/basic.rs index 5182adb..40bbf83 100644 --- a/synth/src/basic.rs +++ b/synth/src/basic.rs @@ -36,7 +36,7 @@ pub fn generate_minimal_repair( 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)?; @@ -44,7 +44,7 @@ pub fn generate_minimal_repair( 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!( @@ -54,8 +54,13 @@ pub fn generate_minimal_repair( } 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", @@ -84,9 +89,9 @@ pub fn generate_minimal_repair( 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))) } diff --git a/synth/src/filters.rs b/synth/src/filters.rs index abfd0f2..f60b3e8 100644 --- a/synth/src/filters.rs +++ b/synth/src/filters.rs @@ -19,11 +19,11 @@ pub fn can_be_repaired_from_arbitrary_state 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, @@ -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<()> { @@ -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(); diff --git a/synth/src/main.rs b/synth/src/main.rs index cbed8a1..8a78dc0 100644 --- a/synth/src/main.rs +++ b/synth/src/main.rs @@ -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, }; diff --git a/synth/src/repair.rs b/synth/src/repair.rs index 9eb1172..f60421d 100644 --- a/synth/src/repair.rs +++ b/synth/src/repair.rs @@ -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, } @@ -45,9 +45,12 @@ pub fn constrain_changes( 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 @@ -63,7 +66,7 @@ pub fn minimize_changes( 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); @@ -72,7 +75,7 @@ pub fn minimize_changes( 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; } } @@ -88,18 +91,18 @@ pub fn constrain_starting_state( { 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_()