From 8a93aae50aaa6d76085f1d6bc654494cc8b3fa2d Mon Sep 17 00:00:00 2001 From: Daniel Kocher Date: Mon, 9 Jan 2023 15:03:52 +0100 Subject: [PATCH 01/19] add: File horizon that implements the horizon extraction when the stride option is enabled --- src/unicorn/horizon.rs | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 src/unicorn/horizon.rs diff --git a/src/unicorn/horizon.rs b/src/unicorn/horizon.rs new file mode 100644 index 00000000..22a252bc --- /dev/null +++ b/src/unicorn/horizon.rs @@ -0,0 +1,26 @@ +use crate::unicorn::{Node, Model}; +use log::warn; + +// +// Public Interface +// + +pub fn print_reasoning_horizon(model: &mut Model, depth: usize, stride: bool) { + let v: Option; + v = match &*model.bad_states_initial[0].borrow() { + Node::Bad { name, ..} => name.clone(), + _ => None + }; + + let ss = v.as_ref().expect("Bad state must have an unrolling depth"); + if let (Some(start), Some(end)) = (ss.find("[n="), ss.find("]")) { + if let (reason, Ok(remainder)) = (ss[..start].to_string(), ss[start+"[n=".len()..end].to_string().parse::()) { + warn!( + "(Initial) Bad state '{}[n={:#?}]' is satisfiable.", + reason, + if stride { (depth - 1) + remainder } else { remainder } + ); + } + + } +} \ No newline at end of file From c3cd965f3df2cffc588a9eccc92c452e5f09c85c Mon Sep 17 00:00:00 2001 From: Daniel Kocher Date: Mon, 9 Jan 2023 15:04:13 +0100 Subject: [PATCH 02/19] add: Stride option --- src/cli.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/cli.rs b/src/cli.rs index 5766b4c5..88749889 100644 --- a/src/cli.rs +++ b/src/cli.rs @@ -244,6 +244,13 @@ pub fn args() -> Command { .allow_hyphen_values(true) .num_args(1..) ) + .arg( + Arg::new("stride") + .help("Find unroll level where SMT solver times out") + .short('l') + .long("stride") + .num_args(0) + ) ) .subcommand( Command::new("qubot") From f70de5019916f9dee2b0828ab06707cfff7def2e Mon Sep 17 00:00:00 2001 From: Daniel Kocher Date: Mon, 9 Jan 2023 15:04:50 +0100 Subject: [PATCH 03/19] feat: Exponential search when the stride option is enabled (up to a max unroll depth) --- src/main.rs | 76 +++++++++++++++++++++++++++++++--------------- src/unicorn/mod.rs | 5 +-- 2 files changed, 55 insertions(+), 26 deletions(-) diff --git a/src/main.rs b/src/main.rs index 3a1d2805..7b11a341 100644 --- a/src/main.rs +++ b/src/main.rs @@ -18,6 +18,7 @@ use crate::unicorn::sat_solver::solve_bad_states; use crate::unicorn::smt_solver::*; use crate::unicorn::unroller::{prune_model, renumber_model, unroll_model}; use crate::unicorn::write_model; +use crate::unicorn::horizon::print_reasoning_horizon; use ::unicorn::disassemble::disassemble; use ::unicorn::emulate::EmulatorState; @@ -33,6 +34,7 @@ use std::{ path::PathBuf, str::FromStr, time::Duration, + cmp::min }; fn main() -> Result<()> { @@ -85,6 +87,7 @@ fn main() -> Result<()> { let input_is_dimacs = !is_beator && args.get_flag("from-dimacs"); let compile_model = is_beator && args.get_flag("compile"); let emulate_model = is_beator && args.get_flag("emulate"); + let stride = args.get_flag("stride"); let arg0 = expect_arg::(args, "input-file")?; let extras = collect_arg_values(args, "extras"); @@ -112,32 +115,57 @@ fn main() -> Result<()> { } else { vec![] }; - for n in 0..unroll_depth { - unroll_model(&mut model, n); - if has_concrete_inputs { - optimize_model_with_input(&mut model, &mut input_values) - } - } - if prune { - prune_model(&mut model); - } + let timeout = solver_timeout.map(|&ms| Duration::from_millis(ms)); - match smt_solver { - #[rustfmt::skip] - SmtType::Generic => { - optimize_model_with_solver::(&mut model, timeout, minimize) - }, - #[rustfmt::skip] - #[cfg(feature = "boolector")] - SmtType::Boolector => { - optimize_model_with_solver::(&mut model, timeout, minimize) - }, - #[rustfmt::skip] - #[cfg(feature = "z3")] - SmtType::Z3 => { - optimize_model_with_solver::(&mut model, timeout, minimize) - }, + + let mut n: usize = if stride { 1 } else { unroll_depth }; + loop { + // TODO: Maybe we can get rid of this clone for each + // iteration, which is basically required if pruning is + // enabled. However, it is much faster this way than + // without pruning and not cloning the model. + let mut model_copy = model.clone(); + + for m in 0..n { + unroll_model(&mut model_copy, m); + + if has_concrete_inputs { + optimize_model_with_input(&mut model_copy, &mut input_values) + } + } + + if prune { + prune_model(&mut model_copy); + } + + match smt_solver { + #[rustfmt::skip] + SmtType::Generic => { + optimize_model_with_solver::(&mut model_copy, timeout, minimize) + }, + #[rustfmt::skip] + #[cfg(feature = "boolector")] + SmtType::Boolector => { + optimize_model_with_solver::(&mut model_copy, timeout, minimize) + }, + #[rustfmt::skip] + #[cfg(feature = "z3")] + SmtType::Z3 => { + optimize_model_with_solver::(&mut model_copy, timeout, minimize) + }, + } + + if !stride || !model_copy.bad_states_initial.is_empty() { + if !model_copy.bad_states_initial.is_empty() { + print_reasoning_horizon(&mut model_copy, n, stride); + } + + break; + } + + n = min(2 * n, unroll_depth); } + if renumber { renumber_model(&mut model); } diff --git a/src/unicorn/mod.rs b/src/unicorn/mod.rs index fdeca318..7e701fd4 100644 --- a/src/unicorn/mod.rs +++ b/src/unicorn/mod.rs @@ -24,11 +24,12 @@ pub mod qubot; pub mod sat_solver; pub mod smt_solver; pub mod unroller; +pub mod horizon; pub type Nid = u64; pub type NodeRef = Rc>; -#[derive(Debug)] +#[derive(Clone,Debug)] pub enum Node { Const { nid: Nid, @@ -176,7 +177,7 @@ pub fn get_nodetype(n: usize) -> NodeType { } } -#[derive(Debug)] +#[derive(Clone, Debug)] pub struct Model { pub lines: Vec, pub sequentials: Vec, From 1cf0b8c4537c6b25d10a6b1625ecf50ceaee0655 Mon Sep 17 00:00:00 2001 From: Daniel Kocher Date: Thu, 12 Jan 2023 11:23:05 +0100 Subject: [PATCH 04/19] fix: Remove Clone from Node type --- src/unicorn/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/unicorn/mod.rs b/src/unicorn/mod.rs index 7e701fd4..8078c90d 100644 --- a/src/unicorn/mod.rs +++ b/src/unicorn/mod.rs @@ -29,7 +29,7 @@ pub mod horizon; pub type Nid = u64; pub type NodeRef = Rc>; -#[derive(Clone,Debug)] +#[derive(Debug)] pub enum Node { Const { nid: Nid, From 29efb58c0992f6ddc47da77956c3db21ce1c65f8 Mon Sep 17 00:00:00 2001 From: Daniel Kocher Date: Thu, 12 Jan 2023 14:09:28 +0100 Subject: [PATCH 05/19] fix: Use absolute depth during unrolling and simplify print_reasoning_horizon --- src/main.rs | 12 +++++++----- src/unicorn/horizon.rs | 15 +++------------ 2 files changed, 10 insertions(+), 17 deletions(-) diff --git a/src/main.rs b/src/main.rs index 7b11a341..9af2fb7b 100644 --- a/src/main.rs +++ b/src/main.rs @@ -118,7 +118,8 @@ fn main() -> Result<()> { let timeout = solver_timeout.map(|&ms| Duration::from_millis(ms)); - let mut n: usize = if stride { 1 } else { unroll_depth }; + let mut n: usize = if stride { 0 } else { unroll_depth }; + let mut prev_n: usize = 0; loop { // TODO: Maybe we can get rid of this clone for each // iteration, which is basically required if pruning is @@ -126,7 +127,7 @@ fn main() -> Result<()> { // without pruning and not cloning the model. let mut model_copy = model.clone(); - for m in 0..n { + for m in prev_n..n { unroll_model(&mut model_copy, m); if has_concrete_inputs { @@ -135,7 +136,7 @@ fn main() -> Result<()> { } if prune { - prune_model(&mut model_copy); + prune_model(&mut model_copy); } match smt_solver { @@ -157,13 +158,14 @@ fn main() -> Result<()> { if !stride || !model_copy.bad_states_initial.is_empty() { if !model_copy.bad_states_initial.is_empty() { - print_reasoning_horizon(&mut model_copy, n, stride); + print_reasoning_horizon(&mut model_copy); } break; } - n = min(2 * n, unroll_depth); + prev_n = n; + n = min(2*n, unroll_depth); } if renumber { diff --git a/src/unicorn/horizon.rs b/src/unicorn/horizon.rs index 22a252bc..84e7c9bf 100644 --- a/src/unicorn/horizon.rs +++ b/src/unicorn/horizon.rs @@ -5,22 +5,13 @@ use log::warn; // Public Interface // -pub fn print_reasoning_horizon(model: &mut Model, depth: usize, stride: bool) { +pub fn print_reasoning_horizon(model: &mut Model) { let v: Option; v = match &*model.bad_states_initial[0].borrow() { Node::Bad { name, ..} => name.clone(), _ => None }; - - let ss = v.as_ref().expect("Bad state must have an unrolling depth"); - if let (Some(start), Some(end)) = (ss.find("[n="), ss.find("]")) { - if let (reason, Ok(remainder)) = (ss[..start].to_string(), ss[start+"[n=".len()..end].to_string().parse::()) { - warn!( - "(Initial) Bad state '{}[n={:#?}]' is satisfiable.", - reason, - if stride { (depth - 1) + remainder } else { remainder } - ); - } - } + let bad_state = v.as_ref().expect("Bad state must have an unrolling depth"); + warn!("(Initial) Bad state '{}' is satisfiable.", bad_state); } \ No newline at end of file From 127d2a9111debf2834bc389164aca5f110dd6b49 Mon Sep 17 00:00:00 2001 From: smml1996 Date: Fri, 20 Jan 2023 21:27:08 +0100 Subject: [PATCH 06/19] feat: adds --one-query flag --- src/cli.rs | 6 ++++++ src/main.rs | 9 +++++---- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/cli.rs b/src/cli.rs index 16bd1475..0438d44b 100644 --- a/src/cli.rs +++ b/src/cli.rs @@ -228,6 +228,12 @@ pub fn args() -> Command { .long("terminate-on-bad") .num_args(0) ) + .arg( + Arg::new("one-query") + .help("Perform only one query for all bad states OR-ed") + .long("one-query") + .num_args(0) + ) .arg( Arg::new("unroll-model") .help("Number of instructions to unroll from model") diff --git a/src/main.rs b/src/main.rs index 59dafaa5..05c16f05 100644 --- a/src/main.rs +++ b/src/main.rs @@ -81,6 +81,7 @@ fn main() -> Result<()> { let minimize = is_beator && !args.get_flag("fast-minimize"); let discretize = !is_beator || args.get_flag("discretize-memory"); let terminate_on_bad = is_beator && args.get_flag("terminate-on-bad"); + let one_query = is_beator && args.get_flag("one-query"); let renumber = !is_beator || output.is_some(); let input_is_btor2 = args.get_flag("from-btor2"); let input_is_dimacs = !is_beator && args.get_flag("from-dimacs"); @@ -126,17 +127,17 @@ fn main() -> Result<()> { match smt_solver { #[rustfmt::skip] SmtType::Generic => { - optimize_model_with_solver::(&mut model, timeout, minimize, terminate_on_bad) + optimize_model_with_solver::(&mut model, timeout, minimize, terminate_on_bad, one_query) }, #[rustfmt::skip] #[cfg(feature = "boolector")] SmtType::Boolector => { - optimize_model_with_solver::(&mut model, timeout, minimize, terminate_on_bad) + optimize_model_with_solver::(&mut model, timeout, minimize, terminate_on_bad, one_query) }, #[rustfmt::skip] #[cfg(feature = "z3")] SmtType::Z3 => { - optimize_model_with_solver::(&mut model, timeout, minimize, terminate_on_bad) + optimize_model_with_solver::(&mut model, timeout, minimize, terminate_on_bad, one_query) }, } if renumber { @@ -194,7 +195,7 @@ fn main() -> Result<()> { let gate_model = bitblast_model(&model.unwrap(), true, 64); if sat_solver != SatType::None { - solve_bad_states(&gate_model, sat_solver, terminate_on_bad)? + solve_bad_states(&gate_model, sat_solver, terminate_on_bad, one_query)? } if output_to_stdout { From a20b44afcc6feb2a804338ac37939528aeb65421 Mon Sep 17 00:00:00 2001 From: smml1996 Date: Fri, 20 Jan 2023 21:56:52 +0100 Subject: [PATCH 07/19] feat: --one-query flag implemented for sat solvers --- src/unicorn/sat_solver.rs | 90 +++++++++++++++++++++++++++++++-------- 1 file changed, 72 insertions(+), 18 deletions(-) diff --git a/src/unicorn/sat_solver.rs b/src/unicorn/sat_solver.rs index f7533bb3..e09c87c6 100644 --- a/src/unicorn/sat_solver.rs +++ b/src/unicorn/sat_solver.rs @@ -1,4 +1,4 @@ -use crate::unicorn::bitblasting::{GateModel, GateRef}; +use crate::unicorn::bitblasting::{GateModel, GateRef, or_gate, Gate, get_constant, is_constant}; use crate::unicorn::{Node, NodeRef}; use crate::SatType; use anyhow::{anyhow, Result}; @@ -13,20 +13,21 @@ pub fn solve_bad_states( gate_model: &GateModel, sat_type: SatType, terminate_on_bad: bool, + one_query: bool ) -> Result<()> { match sat_type { SatType::None => unreachable!(), #[cfg(feature = "kissat")] SatType::Kissat => { - process_all_bad_states::(gate_model, terminate_on_bad) + process_all_bad_states::(gate_model, terminate_on_bad, one_query) } #[cfg(feature = "varisat")] SatType::Varisat => { - process_all_bad_states::(gate_model, terminate_on_bad) + process_all_bad_states::(gate_model, terminate_on_bad, one_query) } #[cfg(feature = "cadical")] SatType::Cadical => { - process_all_bad_states::(gate_model, terminate_on_bad) + process_all_bad_states::(gate_model, terminate_on_bad, one_query) } } } @@ -53,52 +54,105 @@ trait SATSolver { fn process_single_bad_state( solver: &mut S, gate_model: &GateModel, - bad_state: &NodeRef, + bad_state_: Option<&NodeRef>, gate: &GateRef, terminate_on_bad: bool, + one_query: bool ) -> Result<()> { - if let Node::Bad { name, .. } = &*bad_state.borrow() { + if !one_query { + let bad_state = bad_state_.unwrap(); + if let Node::Bad { name, .. } = &*bad_state.borrow() { + let solution = solver.decide(gate_model, gate); + match solution { + SATSolution::Sat => { + warn!( + "Bad state '{}' is satisfiable ({})!", + name.as_deref().unwrap_or("?"), + S::name() + ); + if terminate_on_bad { + return Err(anyhow!("Bad state satisfiable")); + } + } + SATSolution::Unsat => { + debug!( + "Bad state '{}' is unsatisfiable ({}).", + name.as_deref().unwrap_or("?"), + S::name() + ); + } + SATSolution::Timeout => unimplemented!(), + } + Ok(()) + } else { + panic!("expecting 'Bad' node here"); + } + } else { + assert!(bad_state_.is_none()); let solution = solver.decide(gate_model, gate); match solution { SATSolution::Sat => { warn!( - "Bad state '{}' is satisfiable ({})!", - name.as_deref().unwrap_or("?"), + "At least one bad state evaluates to true ({})", S::name() ); - if terminate_on_bad { - return Err(anyhow!("Bad state satisfiable")); - } } SATSolution::Unsat => { debug!( - "Bad state '{}' is unsatisfiable ({}).", - name.as_deref().unwrap_or("?"), + "No bad states occur ({}).", S::name() ); } SATSolution::Timeout => unimplemented!(), } Ok(()) - } else { - panic!("expecting 'Bad' node here"); } + } #[allow(dead_code)] fn process_all_bad_states( gate_model: &GateModel, terminate_on_bad: bool, + one_query: bool ) -> Result<()> { debug!("Using {:?} to decide bad states ...", S::name()); let mut solver = S::new(); - let zip = gate_model + + if !one_query { + let zip = gate_model .bad_state_nodes .iter() .zip(gate_model.bad_state_gates.iter()); - for (bad_state, gate) in zip { - process_single_bad_state(&mut solver, gate_model, bad_state, gate, terminate_on_bad)? + for (bad_state, gate) in zip { + process_single_bad_state(&mut solver, gate_model, Some(bad_state), gate, terminate_on_bad, one_query)? + } + } else { + let mut ored_bad_states: GateRef; + if gate_model.bad_state_gates.len() == 0{ + ored_bad_states = GateRef::from(Gate::ConstFalse); + } else if gate_model.bad_state_gates.len() == 1 { + ored_bad_states = gate_model.bad_state_gates[0]; + } else { + let first_element = gate_model.bad_state_gates[0]; + let second_element = gate_model.bad_state_gates[1]; + ored_bad_states = or_gate(get_constant(&first_element), get_constant(&second_element), &first_element, &second_element); + } + for gate in gate_model.bad_state_gates.iter().skip(2) { + ored_bad_states = or_gate(get_constant(&ored_bad_states), get_constant(gate), &ored_bad_states, gate); + } + if let Some(value) = get_constant(&ored_bad_states ){ + if value { + warn!("Bad state occurs"); + } else { + warn!("No bad state occurs"); + } + } else { + process_single_bad_state(&mut solver, gate_model, None, &ored_bad_states, terminate_on_bad, one_query)? + } + } + Ok(()) } From cdc6d112b6d0bb303e5d7bb96ca4d1517365f4e0 Mon Sep 17 00:00:00 2001 From: smml1996 Date: Fri, 20 Jan 2023 22:10:51 +0100 Subject: [PATCH 08/19] fix: tiny fix sat_solvers --- src/unicorn/sat_solver.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/unicorn/sat_solver.rs b/src/unicorn/sat_solver.rs index e09c87c6..1842cfc0 100644 --- a/src/unicorn/sat_solver.rs +++ b/src/unicorn/sat_solver.rs @@ -132,10 +132,10 @@ fn process_all_bad_states( if gate_model.bad_state_gates.len() == 0{ ored_bad_states = GateRef::from(Gate::ConstFalse); } else if gate_model.bad_state_gates.len() == 1 { - ored_bad_states = gate_model.bad_state_gates[0]; + ored_bad_states = gate_model.bad_state_gates[0].clone(); } else { - let first_element = gate_model.bad_state_gates[0]; - let second_element = gate_model.bad_state_gates[1]; + let first_element = gate_model.bad_state_gates[0].clone(); + let second_element = gate_model.bad_state_gates[1].clone(); ored_bad_states = or_gate(get_constant(&first_element), get_constant(&second_element), &first_element, &second_element); } for gate in gate_model.bad_state_gates.iter().skip(2) { From 66fd80465b73565f3d891c54bac1c787469ab98c Mon Sep 17 00:00:00 2001 From: smml1996 Date: Fri, 20 Jan 2023 22:39:02 +0100 Subject: [PATCH 09/19] feat: --one-query implemented for smt solvers --- src/unicorn/bitblasting.rs | 6 +-- src/unicorn/memory.rs | 5 ++ src/unicorn/mod.rs | 9 ++++ src/unicorn/optimize.rs | 108 +++++++++++++++++++++++++++++++++---- src/unicorn/sat_solver.rs | 92 +++++++++++++++++++------------ src/unicorn/unroller.rs | 13 +++++ 6 files changed, 186 insertions(+), 47 deletions(-) diff --git a/src/unicorn/bitblasting.rs b/src/unicorn/bitblasting.rs index 7c01ef44..c3c11395 100644 --- a/src/unicorn/bitblasting.rs +++ b/src/unicorn/bitblasting.rs @@ -143,11 +143,11 @@ fn get_gate_from_constant_bit(bit: u64) -> GateRef { } } -fn is_constant(gate_type: &GateRef) -> bool { +pub fn is_constant(gate_type: &GateRef) -> bool { matches!(&*gate_type.borrow(), Gate::ConstFalse | Gate::ConstTrue) } -fn get_constant(gate_type: &GateRef) -> Option { +pub fn get_constant(gate_type: &GateRef) -> Option { match &*gate_type.borrow() { Gate::ConstFalse => Some(false), Gate::ConstTrue => Some(true), @@ -313,7 +313,7 @@ fn matriarch1_gate( } } -fn or_gate(a: Option, b: Option, a_gate: &GateRef, b_gate: &GateRef) -> GateRef { +pub fn or_gate(a: Option, b: Option, a_gate: &GateRef, b_gate: &GateRef) -> GateRef { if are_both_constants(a, b) { get_gate_from_boolean(a.unwrap() || b.unwrap()) } else if are_there_true_constants(a, b) { diff --git a/src/unicorn/memory.rs b/src/unicorn/memory.rs index 33849292..30a20813 100644 --- a/src/unicorn/memory.rs +++ b/src/unicorn/memory.rs @@ -300,6 +300,11 @@ impl MemoryReplacer { if let Some(n) = self.visit(right) { *right = n } None } + Node::Or { ref mut left, ref mut right, .. } => { + if let Some(n) = self.visit(left) { *left = n } + if let Some(n) = self.visit(right) { *right = n } + None + } Node::Not { ref mut value, .. } => { if let Some(n) = self.visit(value) { *value = n } None diff --git a/src/unicorn/mod.rs b/src/unicorn/mod.rs index fdeca318..e31e3ff2 100644 --- a/src/unicorn/mod.rs +++ b/src/unicorn/mod.rs @@ -109,6 +109,12 @@ pub enum Node { left: NodeRef, right: NodeRef, }, + Or { + nid: Nid, + sort: NodeType, + left: NodeRef, + right: NodeRef, + }, Not { nid: Nid, sort: NodeType, @@ -248,6 +254,8 @@ where writeln!(out, "{} eq 1 {} {}", nid, get_nid(left), get_nid(right))?, Node::And { nid, sort, left, right } => writeln!(out, "{} and {} {} {}", nid, get_sort(sort), get_nid(left), get_nid(right))?, + Node::Or { nid, sort, left, right } => + writeln!(out, "{} or {} {} {}", nid, get_sort(sort), get_nid(left), get_nid(right))?, Node::Not { nid, sort, value } => writeln!(out, "{} not {} {}", nid, get_sort(sort), get_nid(value))?, Node::State { nid, sort, init, name } => { @@ -296,6 +304,7 @@ pub fn get_nid(node: &NodeRef) -> Nid { Node::Next { nid, .. } => nid, Node::Input { nid, .. } => nid, Node::Bad { nid, .. } => nid, + Node::Or { nid, .. } => nid, Node::Comment(_) => panic!("has no nid"), } } diff --git a/src/unicorn/optimize.rs b/src/unicorn/optimize.rs index b27f4453..94cb7d44 100644 --- a/src/unicorn/optimize.rs +++ b/src/unicorn/optimize.rs @@ -17,16 +17,24 @@ pub fn optimize_model_with_solver( timeout: Option, minimize: bool, terminate_on_bad: bool, + one_query: bool, ) { debug!("Optimizing model using '{}' SMT solver ...", S::name()); debug!("Setting SMT solver timeout to {:?} per query ...", timeout); debug!("Using SMT solver to minimize graph: {} ...", minimize); - optimize_model_impl::(model, &mut vec![], timeout, minimize, terminate_on_bad) + optimize_model_impl::( + model, + &mut vec![], + timeout, + minimize, + terminate_on_bad, + one_query, + ) } pub fn optimize_model_with_input(model: &mut Model, inputs: &mut Vec) { debug!("Optimizing model with {} concrete inputs ...", inputs.len()); - optimize_model_impl::(model, inputs, None, false, false); + optimize_model_impl::(model, inputs, None, false, false, false); } // @@ -39,6 +47,7 @@ fn optimize_model_impl( timeout: Option, minimize: bool, terminate_on_bad: bool, + one_query: bool, ) { let mut constant_folder = ConstantFolder::::new(inputs, timeout, minimize); model @@ -47,12 +56,56 @@ fn optimize_model_impl( for sequential in &model.sequentials { constant_folder.visit(sequential); } - model - .bad_states_initial - .retain(|s| constant_folder.should_retain_bad_state(s, true, terminate_on_bad)); - model - .bad_states_sequential - .retain(|s| constant_folder.should_retain_bad_state(s, false, terminate_on_bad)); + if !one_query { + model.bad_states_initial.retain(|s| { + constant_folder.should_retain_bad_state(s, true, terminate_on_bad, one_query) + }); + model.bad_states_sequential.retain(|s| { + constant_folder.should_retain_bad_state(s, false, terminate_on_bad, one_query) + }); + } else { + model + .bad_states_initial + .retain(|s| constant_folder.should_retain_bad_state(s, false, true, one_query)); + model + .bad_states_sequential + .retain(|s| constant_folder.should_retain_bad_state(s, false, true, one_query)); + + let mut all_bad_states: Vec<&NodeRef> = Vec::new(); + + for bad_state in model.bad_states_initial.iter() { + all_bad_states.push(bad_state); + } + + for bad_state in model.bad_states_sequential.iter() { + all_bad_states.push(bad_state); + } + + if all_bad_states.is_empty() { + panic!("No bad states happen"); + } else if all_bad_states.len() == 1 { + constant_folder.should_retain_bad_state(all_bad_states[0], true, true, false); + panic!("No bad states happen"); + } else { + let mut ored_bad_states = NodeRef::from(Node::Or { + nid: u64::MAX, + sort: NodeType::Bit, + left: all_bad_states[0].clone(), + right: all_bad_states[1].clone(), + }); + + for bad_state in all_bad_states.iter().skip(2) { + ored_bad_states = NodeRef::from(Node::Or { + nid: u64::MAX, + sort: NodeType::Bit, + left: ored_bad_states.clone(), + right: (*bad_state).clone(), + }); + } + + constant_folder.should_retain_bad_state(&ored_bad_states, true, true, true); + } + } } struct ConstantFolder<'a, S> { @@ -339,6 +392,26 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> { self.fold_any_binary(left, right, |a, b| a & b, "AND") } + fn fold_or(&self, left: &NodeRef, right: &NodeRef, sort: &NodeType) -> Option { + if is_const_zeroes(left, sort) { + trace!("Folding OR(zeroes,x) -> x"); + return Some(right.clone()); + } + if is_const_zeroes(right, sort) { + trace!("Folding OR(x,zeroes) -> x"); + return Some(left.clone()); + } + if is_const_ones(left, sort) { + trace!("Strength-reducing AND(ones,_) -> ones"); + return Some(left.clone()); + } + if is_const_ones(right, sort) { + trace!("Strength-reducing AND(x,ones) -> ones"); + return Some(right.clone()); + } + self.fold_any_binary(left, right, |a, b| a | b, "OR") + } + fn solve_and_bit( &mut self, node: &NodeRef, @@ -561,6 +634,11 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> { if let Some(n) = self.visit(right) { *right = n } self.fold_and(left, right, sort) } + Node::Or { ref sort, ref mut left, ref mut right, .. } => { + if let Some(n) = self.visit(left) { *left = n } + if let Some(n) = self.visit(right) { *right = n } + self.fold_or(left, right, sort) + } Node::Not { ref sort, ref mut value, .. } => { if let Some(n) = self.visit(value) { *value = n } self.fold_not(value, sort) @@ -625,6 +703,7 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> { bad_state: &NodeRef, use_smt: bool, terminate_on_bad: bool, + one_query: bool, ) -> bool { self.visit(bad_state); if let Node::Bad { cond, name, .. } = &*bad_state.borrow() { @@ -671,7 +750,18 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> { } true } else { - panic!("expecting 'Bad' node here"); + assert!(one_query); + assert!(use_smt); + match self.smt_solver.solve(bad_state) { + SMTSolution::Sat => { + panic!("Bad states satisfiable"); + } + SMTSolution::Unsat => { + panic!("Bad states unsatisfiable"); + } + SMTSolution::Timeout => (), + } + true } } diff --git a/src/unicorn/sat_solver.rs b/src/unicorn/sat_solver.rs index 1842cfc0..6c97ef2b 100644 --- a/src/unicorn/sat_solver.rs +++ b/src/unicorn/sat_solver.rs @@ -1,4 +1,4 @@ -use crate::unicorn::bitblasting::{GateModel, GateRef, or_gate, Gate, get_constant, is_constant}; +use crate::unicorn::bitblasting::{get_constant, or_gate, Gate, GateModel, GateRef}; use crate::unicorn::{Node, NodeRef}; use crate::SatType; use anyhow::{anyhow, Result}; @@ -13,22 +13,28 @@ pub fn solve_bad_states( gate_model: &GateModel, sat_type: SatType, terminate_on_bad: bool, - one_query: bool + one_query: bool, ) -> Result<()> { match sat_type { SatType::None => unreachable!(), #[cfg(feature = "kissat")] - SatType::Kissat => { - process_all_bad_states::(gate_model, terminate_on_bad, one_query) - } + SatType::Kissat => process_all_bad_states::( + gate_model, + terminate_on_bad, + one_query, + ), #[cfg(feature = "varisat")] - SatType::Varisat => { - process_all_bad_states::(gate_model, terminate_on_bad, one_query) - } + SatType::Varisat => process_all_bad_states::( + gate_model, + terminate_on_bad, + one_query, + ), #[cfg(feature = "cadical")] - SatType::Cadical => { - process_all_bad_states::(gate_model, terminate_on_bad, one_query) - } + SatType::Cadical => process_all_bad_states::( + gate_model, + terminate_on_bad, + one_query, + ), } } @@ -57,7 +63,7 @@ fn process_single_bad_state( bad_state_: Option<&NodeRef>, gate: &GateRef, terminate_on_bad: bool, - one_query: bool + one_query: bool, ) -> Result<()> { if !one_query { let bad_state = bad_state_.unwrap(); @@ -92,67 +98,83 @@ fn process_single_bad_state( let solution = solver.decide(gate_model, gate); match solution { SATSolution::Sat => { - warn!( - "At least one bad state evaluates to true ({})", - S::name() - ); + warn!("At least one bad state evaluates to true ({})", S::name()); } SATSolution::Unsat => { - debug!( - "No bad states occur ({}).", - S::name() - ); + debug!("No bad states occur ({}).", S::name()); } SATSolution::Timeout => unimplemented!(), } Ok(()) } - } #[allow(dead_code)] fn process_all_bad_states( gate_model: &GateModel, terminate_on_bad: bool, - one_query: bool + one_query: bool, ) -> Result<()> { debug!("Using {:?} to decide bad states ...", S::name()); let mut solver = S::new(); - + if !one_query { let zip = gate_model - .bad_state_nodes - .iter() - .zip(gate_model.bad_state_gates.iter()); + .bad_state_nodes + .iter() + .zip(gate_model.bad_state_gates.iter()); for (bad_state, gate) in zip { - process_single_bad_state(&mut solver, gate_model, Some(bad_state), gate, terminate_on_bad, one_query)? + process_single_bad_state( + &mut solver, + gate_model, + Some(bad_state), + gate, + terminate_on_bad, + one_query, + )? } } else { let mut ored_bad_states: GateRef; - if gate_model.bad_state_gates.len() == 0{ + if gate_model.bad_state_gates.is_empty() { ored_bad_states = GateRef::from(Gate::ConstFalse); } else if gate_model.bad_state_gates.len() == 1 { ored_bad_states = gate_model.bad_state_gates[0].clone(); } else { let first_element = gate_model.bad_state_gates[0].clone(); let second_element = gate_model.bad_state_gates[1].clone(); - ored_bad_states = or_gate(get_constant(&first_element), get_constant(&second_element), &first_element, &second_element); + ored_bad_states = or_gate( + get_constant(&first_element), + get_constant(&second_element), + &first_element, + &second_element, + ); } for gate in gate_model.bad_state_gates.iter().skip(2) { - ored_bad_states = or_gate(get_constant(&ored_bad_states), get_constant(gate), &ored_bad_states, gate); - } - if let Some(value) = get_constant(&ored_bad_states ){ + ored_bad_states = or_gate( + get_constant(&ored_bad_states), + get_constant(gate), + &ored_bad_states, + gate, + ); + } + if let Some(value) = get_constant(&ored_bad_states) { if value { warn!("Bad state occurs"); } else { warn!("No bad state occurs"); } } else { - process_single_bad_state(&mut solver, gate_model, None, &ored_bad_states, terminate_on_bad, one_query)? + process_single_bad_state( + &mut solver, + gate_model, + None, + &ored_bad_states, + terminate_on_bad, + one_query, + )? } - } - + Ok(()) } diff --git a/src/unicorn/unroller.rs b/src/unicorn/unroller.rs index 66dac34c..134cea68 100644 --- a/src/unicorn/unroller.rs +++ b/src/unicorn/unroller.rs @@ -172,6 +172,11 @@ impl ModelRenumberer { self.visit(right); self.next_nid(nid); } + Node::Or { ref mut nid, ref left, ref right, .. } => { + self.visit(left); + self.visit(right); + self.next_nid(nid); + } Node::Not { ref mut nid, ref value, .. } => { self.visit(value); self.next_nid(nid); @@ -330,6 +335,14 @@ impl ModelUnroller { right: self.unroll(right), })) } + Node::Or { sort, left, right, .. } => { + Rc::new(RefCell::new(Node::Or { + nid: 0, + sort: sort.clone(), + left: self.unroll(left), + right: self.unroll(right), + })) + } Node::Not { sort, value, .. } => { Rc::new(RefCell::new(Node::Not { nid: 0, From 9ebe416ae3d9f2558edb04aff4d5f4fb409adc89 Mon Sep 17 00:00:00 2001 From: smml1996 Date: Fri, 20 Jan 2023 22:44:07 +0100 Subject: [PATCH 10/19] fix: add Node::or handle for smt solvers --- src/unicorn/smt_solver.rs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/unicorn/smt_solver.rs b/src/unicorn/smt_solver.rs index 8fff4e04..66a1814c 100644 --- a/src/unicorn/smt_solver.rs +++ b/src/unicorn/smt_solver.rs @@ -240,6 +240,11 @@ pub mod boolector_impl { let bv_right = self.visit(right).into_bv(); bv_left.and(&bv_right).into() } + Node::Or { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left.or(&bv_right).into() + } Node::Not { value, .. } => { let bv_value = self.visit(value).into_bv(); bv_value.not().into() @@ -466,6 +471,16 @@ pub mod z3solver_impl { let z3_right = self.visit(right).as_bv().expect("bv"); z3_left.bvand(&z3_right).into() } + Node::Or { sort: NodeType::Bit, left, right, .. } => { + let z3_left = self.visit(left).as_bool().expect("bool"); + let z3_right = self.visit(right).as_bool().expect("bool"); + Bool::or(self.context, &[&z3_left, &z3_right]).into() + } + Node::Or { left, right, .. } => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left.bvor(&z3_right).into() + } Node::Not { value, .. } => { let z3_value = self.visit(value).as_bool().expect("bool"); z3_value.not().into() From 5f7d495e01f35ad4c3380d50fd136e74eb208f55 Mon Sep 17 00:00:00 2001 From: smml1996 Date: Fri, 20 Jan 2023 22:58:30 +0100 Subject: [PATCH 11/19] fix: Node::Bad is now reachable in solvers --- src/unicorn/optimize.rs | 4 ++-- src/unicorn/smt_solver.rs | 8 ++++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/unicorn/optimize.rs b/src/unicorn/optimize.rs index 94cb7d44..0d322829 100644 --- a/src/unicorn/optimize.rs +++ b/src/unicorn/optimize.rs @@ -61,7 +61,7 @@ fn optimize_model_impl( constant_folder.should_retain_bad_state(s, true, terminate_on_bad, one_query) }); model.bad_states_sequential.retain(|s| { - constant_folder.should_retain_bad_state(s, false, terminate_on_bad, one_query) + constant_folder.should_retain_bad_state(s, true, terminate_on_bad, one_query) }); } else { model @@ -102,7 +102,7 @@ fn optimize_model_impl( right: (*bad_state).clone(), }); } - + println!("bad states len {}", all_bad_states.len()); constant_folder.should_retain_bad_state(&ored_bad_states, true, true, true); } } diff --git a/src/unicorn/smt_solver.rs b/src/unicorn/smt_solver.rs index 66a1814c..001a6877 100644 --- a/src/unicorn/smt_solver.rs +++ b/src/unicorn/smt_solver.rs @@ -261,7 +261,9 @@ pub mod boolector_impl { BV::new(self.solver.clone(), width, Some(name)).into() } Node::Next { .. } => panic!("should be unreachable"), - Node::Bad { .. } => panic!("should be unreachable"), + Node::Bad { cond, .. } => { + self.visit(cond) + }, Node::Comment(_) => panic!("cannot translate"), } } @@ -504,7 +506,9 @@ pub mod z3solver_impl { BV::new_const(self.context, name.to_owned(), width).into() } Node::Next { .. } => panic!("should be unreachable"), - Node::Bad { .. } => panic!("should be unreachable"), + Node::Bad { cond, .. } => { + self.visit(cond).clone() + }, Node::Comment(_) => panic!("cannot translate"), } } From 53e52032fbfbf6903adca34e514dab61848181f4 Mon Sep 17 00:00:00 2001 From: smml1996 Date: Sun, 22 Jan 2023 15:34:34 +0100 Subject: [PATCH 12/19] fix: --one-query does not checks on bad states sequential --- src/unicorn/optimize.rs | 54 ++++++++++++----------------------------- 1 file changed, 16 insertions(+), 38 deletions(-) diff --git a/src/unicorn/optimize.rs b/src/unicorn/optimize.rs index 0d322829..fc6e08df 100644 --- a/src/unicorn/optimize.rs +++ b/src/unicorn/optimize.rs @@ -58,43 +58,30 @@ fn optimize_model_impl( } if !one_query { model.bad_states_initial.retain(|s| { - constant_folder.should_retain_bad_state(s, true, terminate_on_bad, one_query) + constant_folder.should_retain_bad_state(s, true, terminate_on_bad) }); model.bad_states_sequential.retain(|s| { - constant_folder.should_retain_bad_state(s, true, terminate_on_bad, one_query) + constant_folder.should_retain_bad_state(s, true, terminate_on_bad) }); } else { model .bad_states_initial - .retain(|s| constant_folder.should_retain_bad_state(s, false, true, one_query)); - model - .bad_states_sequential - .retain(|s| constant_folder.should_retain_bad_state(s, false, true, one_query)); - - let mut all_bad_states: Vec<&NodeRef> = Vec::new(); - - for bad_state in model.bad_states_initial.iter() { - all_bad_states.push(bad_state); - } - - for bad_state in model.bad_states_sequential.iter() { - all_bad_states.push(bad_state); - } + .retain(|s| constant_folder.should_retain_bad_state(s, false, true)); - if all_bad_states.is_empty() { + if model.bad_states_initial.is_empty() { panic!("No bad states happen"); - } else if all_bad_states.len() == 1 { - constant_folder.should_retain_bad_state(all_bad_states[0], true, true, false); + } else if model.bad_states_initial.len() == 1 { + constant_folder.should_retain_bad_state(&model.bad_states_initial[0], true, true); panic!("No bad states happen"); } else { let mut ored_bad_states = NodeRef::from(Node::Or { nid: u64::MAX, sort: NodeType::Bit, - left: all_bad_states[0].clone(), - right: all_bad_states[1].clone(), + left: model.bad_states_initial[0].clone(), + right: model.bad_states_initial[1].clone(), }); - for bad_state in all_bad_states.iter().skip(2) { + for bad_state in model.bad_states_initial.iter().skip(2) { ored_bad_states = NodeRef::from(Node::Or { nid: u64::MAX, sort: NodeType::Bit, @@ -102,8 +89,11 @@ fn optimize_model_impl( right: (*bad_state).clone(), }); } - println!("bad states len {}", all_bad_states.len()); - constant_folder.should_retain_bad_state(&ored_bad_states, true, true, true); + if !constant_folder.smt_solver.is_always_false(&ored_bad_states) { + panic!("bad states are satisfiable!") + } else { + panic!("No bad state happen.") + } } } } @@ -702,8 +692,7 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> { &mut self, bad_state: &NodeRef, use_smt: bool, - terminate_on_bad: bool, - one_query: bool, + terminate_on_bad: bool ) -> bool { self.visit(bad_state); if let Node::Bad { cond, name, .. } = &*bad_state.borrow() { @@ -750,18 +739,7 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> { } true } else { - assert!(one_query); - assert!(use_smt); - match self.smt_solver.solve(bad_state) { - SMTSolution::Sat => { - panic!("Bad states satisfiable"); - } - SMTSolution::Unsat => { - panic!("Bad states unsatisfiable"); - } - SMTSolution::Timeout => (), - } - true + panic!("Expecting Bad node here!") } } From c0757df685ef5a889c36fe8123e1f5cedfc9fdd8 Mon Sep 17 00:00:00 2001 From: smml1996 Date: Sun, 22 Jan 2023 15:45:28 +0100 Subject: [PATCH 13/19] refactor: cargo fmt --- src/unicorn/optimize.rs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/unicorn/optimize.rs b/src/unicorn/optimize.rs index fc6e08df..1e13f0b8 100644 --- a/src/unicorn/optimize.rs +++ b/src/unicorn/optimize.rs @@ -57,12 +57,12 @@ fn optimize_model_impl( constant_folder.visit(sequential); } if !one_query { - model.bad_states_initial.retain(|s| { - constant_folder.should_retain_bad_state(s, true, terminate_on_bad) - }); - model.bad_states_sequential.retain(|s| { - constant_folder.should_retain_bad_state(s, true, terminate_on_bad) - }); + model + .bad_states_initial + .retain(|s| constant_folder.should_retain_bad_state(s, true, terminate_on_bad)); + model + .bad_states_sequential + .retain(|s| constant_folder.should_retain_bad_state(s, true, terminate_on_bad)); } else { model .bad_states_initial @@ -692,7 +692,7 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> { &mut self, bad_state: &NodeRef, use_smt: bool, - terminate_on_bad: bool + terminate_on_bad: bool, ) -> bool { self.visit(bad_state); if let Node::Bad { cond, name, .. } = &*bad_state.borrow() { From 920c499f68ee5be6db873d42ed0ae199094b2d12 Mon Sep 17 00:00:00 2001 From: smml1996 Date: Sun, 22 Jan 2023 15:46:13 +0100 Subject: [PATCH 14/19] chore: add assertion for minimize when --one-query flag is used --- src/unicorn/optimize.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/unicorn/optimize.rs b/src/unicorn/optimize.rs index 1e13f0b8..5aee8c10 100644 --- a/src/unicorn/optimize.rs +++ b/src/unicorn/optimize.rs @@ -64,6 +64,7 @@ fn optimize_model_impl( .bad_states_sequential .retain(|s| constant_folder.should_retain_bad_state(s, true, terminate_on_bad)); } else { + assert!(!minimize); // only works with the --fast-minimize flag model .bad_states_initial .retain(|s| constant_folder.should_retain_bad_state(s, false, true)); From 3088960dcee3beffc30501ed157f0b822a87c9bd Mon Sep 17 00:00:00 2001 From: Daniel Kocher Date: Mon, 23 Jan 2023 15:34:32 +0100 Subject: [PATCH 15/19] chore: Resolve merge conflict --- src/cli.rs | 22 +++++-- src/main.rs | 88 +++++++++++++++----------- src/unicorn/horizon.rs | 129 +++++++++++++++++++++++++++++++++++++- src/unicorn/optimize.rs | 75 +++++++++++++++++++++- src/unicorn/smt_solver.rs | 17 +++++ 5 files changed, 286 insertions(+), 45 deletions(-) diff --git a/src/cli.rs b/src/cli.rs index a91836f0..14a1eee2 100644 --- a/src/cli.rs +++ b/src/cli.rs @@ -259,11 +259,23 @@ pub fn args() -> Command { .num_args(1..) ) .arg( - Arg::new("stride") - .help("Find unroll level where SMT solver times out") - .short('l') - .long("stride") - .num_args(0) + Arg::new("stride") + .help("Find unroll level where SMT solver times out") + .short('l') + .long("stride") + .num_args(0) + // TODO: Set base via argument + // .value_name("NUMBER") + // .value_parser(value_parser!(u64)), + ) + .arg( + Arg::new("time-budget") + .help("Set an overall time budget in milliseconds") + .short('g') + .long("time-budget") + .num_args(1) + .value_name("NUMBER") + .value_parser(value_parser!(u64)) ) ) .subcommand( diff --git a/src/main.rs b/src/main.rs index e38c0032..ca8fe025 100644 --- a/src/main.rs +++ b/src/main.rs @@ -12,13 +12,17 @@ use crate::unicorn::codegen::compile_model_into_program; use crate::unicorn::dimacs_parser::load_dimacs_as_gatemodel; use crate::unicorn::emulate_loader::load_model_into_emulator; use crate::unicorn::memory::replace_memory; -use crate::unicorn::optimize::{optimize_model_with_input, optimize_model_with_solver}; +use crate::unicorn::optimize::{optimize_model_with_input, optimize_model_with_solver, optimize_model_with_solver_n}; use crate::unicorn::qubot::{InputEvaluator, Qubot}; use crate::unicorn::sat_solver::solve_bad_states; use crate::unicorn::smt_solver::*; use crate::unicorn::unroller::{prune_model, renumber_model, unroll_model}; use crate::unicorn::write_model; -use crate::unicorn::horizon::print_reasoning_horizon; +use crate::unicorn::horizon::{ + reason, + reason_backwards, + print_reasoning_horizon +}; use ::unicorn::disassemble::disassemble; use ::unicorn::emulate::EmulatorState; @@ -34,9 +38,12 @@ use std::{ path::PathBuf, str::FromStr, time::Duration, + time::Instant, cmp::min }; +use log::warn; + fn main() -> Result<()> { let matches = cli::args().get_matches(); @@ -90,6 +97,7 @@ fn main() -> Result<()> { let compile_model = is_beator && args.get_flag("compile"); let emulate_model = is_beator && args.get_flag("emulate"); let stride = args.get_flag("stride"); + let solver_time_budget = args.get_one::("time-budget"); let arg0 = expect_arg::(args, "input-file")?; let extras = collect_arg_values(args, "extras"); @@ -119,53 +127,57 @@ fn main() -> Result<()> { }; let timeout = solver_timeout.map(|&ms| Duration::from_millis(ms)); + + let mut time_budget = solver_time_budget.map( + |&ms| Duration::from_millis(ms) + ); + + // TODO: Refactor the subsequent loop (reasoning horizon) - let mut n: usize = if stride { 0 } else { unroll_depth }; + let mut n: usize = if stride { 1 } else { unroll_depth }; let mut prev_n: usize = 0; loop { - // TODO: Maybe we can get rid of this clone for each - // iteration, which is basically required if pruning is - // enabled. However, it is much faster this way than - // without pruning and not cloning the model. - let mut model_copy = model.clone(); - - for m in prev_n..n { - unroll_model(&mut model_copy, m); - - if has_concrete_inputs { - optimize_model_with_input(&mut model_copy, &mut input_values) - } - } - - if prune { - prune_model(&mut model_copy); - } + let mut elapsed = reason( + &mut model, + has_concrete_inputs, + &mut input_values, + prev_n, + n, + prune, + &smt_solver, + timeout, + minimize + ); - match smt_solver { - #[rustfmt::skip] - SmtType::Generic => { - optimize_model_with_solver::(&mut model_copy, timeout, minimize, terminate_on_bad, one_query) - }, - #[rustfmt::skip] - #[cfg(feature = "boolector")] - SmtType::Boolector => { - optimize_model_with_solver::(&mut model_copy, timeout, minimize, terminate_on_bad, one_query) - }, - #[rustfmt::skip] - #[cfg(feature = "z3")] - SmtType::Z3 => { - optimize_model_with_solver::(&mut model_copy, timeout, minimize, terminate_on_bad, one_query) - }, + if time_budget.unwrap() < elapsed { + let r = reason_backwards( + &mut model, + has_concrete_inputs, + &mut input_values, + prev_n, + n, + prune, + &smt_solver, + timeout, + minimize, + &mut time_budget.unwrap() + ); + + warn!("We can reason until depth n = {}", r); + break; } - if !stride || !model_copy.bad_states_initial.is_empty() { - if !model_copy.bad_states_initial.is_empty() { - print_reasoning_horizon(&mut model_copy); + if !stride || !model.bad_states_initial.is_empty() { + if !model.bad_states_initial.is_empty() { + print_reasoning_horizon(&mut model); } break; } + time_budget = Some(time_budget.unwrap() - elapsed); + warn!("Remaining time budget: {:#?} ...", time_budget.unwrap()); + prev_n = n; n = min(2*n, unroll_depth); } diff --git a/src/unicorn/horizon.rs b/src/unicorn/horizon.rs index 84e7c9bf..1b1734ec 100644 --- a/src/unicorn/horizon.rs +++ b/src/unicorn/horizon.rs @@ -1,10 +1,31 @@ use crate::unicorn::{Node, Model}; -use log::warn; +use crate::cli::{SatType, SmtType}; +use crate::unicorn::unroller::{prune_model, renumber_model, unroll_model}; +use crate::unicorn::optimize::{ + optimize_model_with_input, + optimize_model_with_solver, + optimize_model_with_solver_n +}; +use crate::unicorn::smt_solver::*; + +use log::{debug, warn}; +use std::{ + cmp::min, + time::{Duration,Instant}, +}; // // Public Interface // +// pub fn foo(&mut model: Model, &input_values: Vec, &smt_solver: SmtType, unroll_depth: usize, &time_budget: Option, prune: bool, stride: bool) { + +// } + +// +// Private Interface +// + pub fn print_reasoning_horizon(model: &mut Model) { let v: Option; v = match &*model.bad_states_initial[0].borrow() { @@ -14,4 +35,110 @@ pub fn print_reasoning_horizon(model: &mut Model) { let bad_state = v.as_ref().expect("Bad state must have an unrolling depth"); warn!("(Initial) Bad state '{}' is satisfiable.", bad_state); +} + +pub fn reason( + model: &mut Model, + has_concrete_inputs: bool, + input_values: &mut Vec, + start: usize, + end: usize, + prune: bool, + smt_solver: &SmtType, + timeout: Option, + minimize: bool +) -> Duration { + // TODO: Maybe we can get rid of this clone for each + // iteration, which is basically required if pruning is + // enabled. However, it is much faster this way than + // without pruning and not cloning the model. + let mut model_copy = model.clone(); + + let mut now = Instant::now(); + + for m in start..end { + unroll_model(&mut model_copy, m); + + if has_concrete_inputs { + optimize_model_with_input(&mut model_copy, input_values) + } + } + + if prune { + prune_model(&mut model_copy); + } + + match smt_solver { + #[rustfmt::skip] + SmtType::Generic => { + optimize_model_with_solver_n::(&mut model_copy, timeout, minimize) + }, + #[rustfmt::skip] + #[cfg(feature = "boolector")] + SmtType::Boolector => { + optimize_model_with_solver_n::(&mut model_copy, timeout, minimize) + }, + #[rustfmt::skip] + #[cfg(feature = "z3")] + SmtType::Z3 => { + optimize_model_with_solver_n::(&mut model_copy, timeout, minimize) + }, + } + + now.elapsed() +} + +pub fn reason_backwards( + model: &mut Model, + has_concrete_inputs: bool, + input_values: &mut Vec, + prev_n: usize, + n: usize, + prune: bool, + smt_solver: &SmtType, + timeout: Option, + minimize: bool, + time_budget: &mut Duration, +) -> usize { + // warn!("Used up time budget of {:#?} somwhere in between the last {} steps", solver_time_budget.map(|&ms| Duration::from_millis(ms)).unwrap(), n-prev_n); + debug!("Backwards reasoning (binary search) ..."); + + let mut start: usize = prev_n; + let mut end: usize = n; + let mut last_timeout: usize = n; + while start <= end { + let mid: usize = (start + end)/2; + + let elapsed = reason( + model, + has_concrete_inputs, + input_values, + start, + mid, + prune, + &smt_solver, + timeout, + minimize); + + if *time_budget < elapsed { + end = mid - 1; + last_timeout = mid; + debug!("Elapsed: {:#?}", elapsed); + } else if *time_budget > elapsed + && last_timeout > mid { + start = mid + 1; + + *time_budget = *time_budget - elapsed; + debug!("Elapsed: {:#?}", elapsed); + } + + if *time_budget == elapsed + || mid + 1 == last_timeout { + return mid; + } + + debug!("New steps: {} - {} ...", start, end); + debug!("Remaining time budget: {:#?} ...", time_budget); + } + panic!("No result during backwards reasoning") } \ No newline at end of file diff --git a/src/unicorn/optimize.rs b/src/unicorn/optimize.rs index 5aee8c10..5a2af47d 100644 --- a/src/unicorn/optimize.rs +++ b/src/unicorn/optimize.rs @@ -32,6 +32,18 @@ pub fn optimize_model_with_solver( ) } +pub fn optimize_model_with_solver_n( + model: &mut Model, + timeout: Option, + minimize: bool +) { + debug!("Optimizing model using '{}' SMT solver ...", S::name()); + debug!("Setting SMT solver timeout to {:?} per query ...", timeout); + debug!("Using SMT solver to minimize graph: {} ...", minimize); + debug!("Optimizing {} steps at once ....", model.bad_states_initial.len()); + optimize_model_impl_n::(model, &mut vec![], timeout, minimize); +} + pub fn optimize_model_with_input(model: &mut Model, inputs: &mut Vec) { debug!("Optimizing model with {} concrete inputs ...", inputs.len()); optimize_model_impl::(model, inputs, None, false, false, false); @@ -99,6 +111,30 @@ fn optimize_model_impl( } } +fn optimize_model_impl_n( + model: &mut Model, + inputs: &mut Vec, + timeout: Option, + minimize: bool +) { + let mut constant_folder = + ConstantFolder::::new(inputs, timeout, minimize); + model + .sequentials + .retain(|s| constant_folder.should_retain_sequential(s)); + for sequential in &model.sequentials { + constant_folder.visit(sequential); + } + model + .bad_states_initial + .retain(|s| constant_folder.should_retain_bad_state(s, false)); + + constant_folder.should_retain_bad_states(&mut model.bad_states_initial, true); // ? + model + .bad_states_sequential + .retain(|s| constant_folder.should_retain_bad_state(s, false)); +} + struct ConstantFolder<'a, S> { smt_solver: S, marks: HashSet, @@ -699,7 +735,7 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> { if let Node::Bad { cond, name, .. } = &*bad_state.borrow() { if is_const_false(cond) { debug!( - "Bad state '{}' became unreachable, removing", + "Bad state '{}' became statically unreachable, removing", name.as_deref().unwrap_or("?") ); return false; @@ -744,6 +780,43 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> { } } + fn should_retain_bad_states(&mut self, bad_states: &Vec, use_smt: bool) -> bool { + debug!("bad_states_initial.len() = {}", bad_states.len()); + + let mut conds: Vec = Vec::new(); + + for bad_state in bad_states.iter() { + self.visit(bad_state); + + let v = &*bad_state.borrow(); + if let Node::Bad { cond, .. } = v { + conds.push(cond.clone()); + } + } + + if use_smt { + match self.smt_solver.solve_n(&conds) { + SMTSolution::Sat => { + // warn!( + // "A bad state '{}' is satisfiable within the last {} unrollings!", + // name.as_deref().unwrap_or("?"), + // conds.len() + // ); + return true; + } + SMTSolution::Unsat => { + // debug!( + // "Bad state '{}' is unsatisfiable , removing", + // name.as_deref().unwrap_or("?") + // ); + return false; + } + SMTSolution::Timeout => (), + } + } + true + } + fn should_retain_sequential(&mut self, sequential: &NodeRef) -> bool { if let Node::Next { state, next, .. } = &*sequential.borrow() { if let Node::State { init, name, .. } = &*state.borrow() { diff --git a/src/unicorn/smt_solver.rs b/src/unicorn/smt_solver.rs index 001a6877..26d018d3 100644 --- a/src/unicorn/smt_solver.rs +++ b/src/unicorn/smt_solver.rs @@ -20,6 +20,7 @@ pub trait SMTSolver { fn new(timeout: Option) -> Self; fn name() -> &'static str; fn solve(&mut self, root: &NodeRef) -> SMTSolution; + fn solve_n(&mut self, nodes: &Vec) -> SMTSolution; fn is_always_true(&mut self, node: &NodeRef) -> bool; fn is_always_false(&mut self, node: &NodeRef) -> bool; fn is_always_equal(&mut self, left: &NodeRef, right: &NodeRef) -> bool; @@ -61,6 +62,10 @@ pub mod none_impl { fn solve(&mut self, _root: &NodeRef) -> SMTSolution { SMTSolution::Timeout } + + fn solve_n(&mut self, _nodes: &Vec) -> SMTSolution { + SMTSolution::Timeout + } } } @@ -131,6 +136,14 @@ pub mod boolector_impl { let bv = self.visit(root).into_bv(); self.solve_impl(bv.slice(0, 0)) } + + fn solve_n(&mut self, nodes: &Vec) -> SMTSolution { + let bv = BV::zero(self.solver.clone(), 1); + for node in nodes.iter() { + bv.or(&self.visit(node).into_bv()); + } + self.solve_impl(bv) + } } impl BoolectorSolver { @@ -362,6 +375,10 @@ pub mod z3solver_impl { let z3_bool = self.visit(root).as_bool().expect("bool"); self.solve_impl(&z3_bool) } + + fn solve_n(&mut self, _nodes: &Vec) -> SMTSolution { + SMTSolution::Timeout + } } impl<'ctx> Z3SolverWrapper<'ctx> { From 8c23cf0ab5af35d7327f9530ecdd438d4cdb1e63 Mon Sep 17 00:00:00 2001 From: Daniel Kocher Date: Tue, 24 Jan 2023 16:47:43 +0100 Subject: [PATCH 16/19] chore: Resolve merge conflict --- src/unicorn/horizon.rs | 238 +++++++++++++++++++++++++++++----------- src/unicorn/optimize.rs | 37 ------- 2 files changed, 172 insertions(+), 103 deletions(-) diff --git a/src/unicorn/horizon.rs b/src/unicorn/horizon.rs index 1b1734ec..0ea2229a 100644 --- a/src/unicorn/horizon.rs +++ b/src/unicorn/horizon.rs @@ -1,40 +1,100 @@ -use crate::unicorn::{Node, Model}; -use crate::cli::{SatType, SmtType}; -use crate::unicorn::unroller::{prune_model, renumber_model, unroll_model}; +use crate::unicorn::{Node, NodeRef, Model}; +use crate::cli::{SmtType}; +use crate::unicorn::unroller::{prune_model, unroll_model}; use crate::unicorn::optimize::{ optimize_model_with_input, optimize_model_with_solver, - optimize_model_with_solver_n + // optimize_model_with_solver_n }; use crate::unicorn::smt_solver::*; use log::{debug, warn}; use std::{ - cmp::min, - time::{Duration,Instant}, + cmp::min, + time::{Duration,Instant} }; // // Public Interface // -// pub fn foo(&mut model: Model, &input_values: Vec, &smt_solver: SmtType, unroll_depth: usize, &time_budget: Option, prune: bool, stride: bool) { +pub fn compute_reasoning_horizon( + model: &mut Model, + has_concrete_inputs: bool, + input_values: &mut Vec, + unroll_depth: usize, + prune: bool, + stride: bool, + smt_solver: &SmtType, + timeout: Option, + minimize: bool, + terminate_on_bad: bool, + one_query: bool, + time_budget: &mut Option +) { + let has_time_budget = !time_budget.is_none(); + + let mut n: usize = if stride { 1 } else { unroll_depth }; + let mut prev_n: usize = 0; + + let mut exec_time = Duration::from_millis(0); + + loop { + // TODO(1): Maybe we can get rid of this clone for each + // iteration, which is basically required if pruning is + // enabled. However, it is much faster this way than + // without pruning and not cloning the model. + let (elapsed, bad_states_initial) = reason( + &mut model.clone(), + has_concrete_inputs, + input_values, + prev_n, + n, + prune, + &smt_solver, + timeout, + minimize, + terminate_on_bad, + one_query + ); + + exec_time += elapsed; + + if has_time_budget && time_budget.unwrap() < exec_time { + // TODO(2): Cf. TODO(1) + let r = reason_backwards( + &mut model.clone(), + &bad_states_initial, + prev_n, + n, + prune, + &smt_solver, + timeout, + minimize, + terminate_on_bad, + one_query, + &(time_budget.unwrap() - exec_time) + ); + + warn!("Depth [n={}] (in {:#?})", r.0, exec_time - elapsed + r.1); + break; + } -// } + if !stride || !model.bad_states_initial.is_empty() { + if !model.bad_states_initial.is_empty() { + print_reasoning_horizon(model); + } -// -// Private Interface -// + break; + } -pub fn print_reasoning_horizon(model: &mut Model) { - let v: Option; - v = match &*model.bad_states_initial[0].borrow() { - Node::Bad { name, ..} => name.clone(), - _ => None - }; - - let bad_state = v.as_ref().expect("Bad state must have an unrolling depth"); - warn!("(Initial) Bad state '{}' is satisfiable.", bad_state); + if has_time_budget { + debug!("Remaining time budget: {:#?} ...", time_budget.unwrap() - exec_time); + } + + prev_n = n; + n = min(2*n, unroll_depth); + } } pub fn reason( @@ -46,99 +106,145 @@ pub fn reason( prune: bool, smt_solver: &SmtType, timeout: Option, - minimize: bool -) -> Duration { - // TODO: Maybe we can get rid of this clone for each - // iteration, which is basically required if pruning is - // enabled. However, it is much faster this way than - // without pruning and not cloning the model. - let mut model_copy = model.clone(); + minimize: bool, + terminate_on_bad: bool, + one_query: bool +) -> (Duration, Vec) { + let now = Instant::now(); - let mut now = Instant::now(); + debug!("Model (initial):\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); for m in start..end { - unroll_model(&mut model_copy, m); + unroll_model(model, m); if has_concrete_inputs { - optimize_model_with_input(&mut model_copy, input_values) + optimize_model_with_input(model, input_values) } } + debug!("Model (after unrolling):\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); + if prune { - prune_model(&mut model_copy); + prune_model(model); } + debug!("Model (after pruning):\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); + + let bad_states_initial = model.bad_states_initial.clone(); + match smt_solver { #[rustfmt::skip] SmtType::Generic => { - optimize_model_with_solver_n::(&mut model_copy, timeout, minimize) + optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query) }, #[rustfmt::skip] #[cfg(feature = "boolector")] SmtType::Boolector => { - optimize_model_with_solver_n::(&mut model_copy, timeout, minimize) + optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query) }, #[rustfmt::skip] #[cfg(feature = "z3")] SmtType::Z3 => { - optimize_model_with_solver_n::(&mut model_copy, timeout, minimize) + optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query) }, } - now.elapsed() + debug!("Model (after SMT solver query):\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); + + (now.elapsed(), bad_states_initial) } pub fn reason_backwards( model: &mut Model, - has_concrete_inputs: bool, - input_values: &mut Vec, + bad_states_initial: &Vec, prev_n: usize, n: usize, prune: bool, smt_solver: &SmtType, timeout: Option, minimize: bool, - time_budget: &mut Duration, -) -> usize { - // warn!("Used up time budget of {:#?} somwhere in between the last {} steps", solver_time_budget.map(|&ms| Duration::from_millis(ms)).unwrap(), n-prev_n); - debug!("Backwards reasoning (binary search) ..."); + terminate_on_bad: bool, + one_query: bool, + time_budget: &Duration, +) -> (usize, Duration) { + // warn!("Used up time budget of {:#?} somwhere in between the last {} steps", solver_time_budget.map(|&ms| Duration::from_millis(ms)).unwrap(), n-prev_n); + + debug!("Model (before pruning):\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); + + if prune { + prune_model(model) + } + + debug!("Model (after pruning):\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); + + + debug!("Backwards reasoning (binary search) for the last {} bad states ...", bad_states_initial.len()); let mut start: usize = prev_n; let mut end: usize = n; - let mut last_timeout: usize = n; + + let mut last_n: usize = n; + let mut last_exec_time = Duration::from_millis(0); + while start <= end { - let mid: usize = (start + end)/2; + let mid: usize = (start + end)/2; + + debug!("Try to fit remaining time budget {:#?} into {} steps ({} to {})...", time_budget, mid-prev_n, prev_n, mid); + + let now = Instant::now(); + + model.bad_states_initial = + bad_states_initial.clone()[(prev_n - (mid-prev_n)) * 10..].to_vec(); + + debug!("Calling SMT solver with the last {} bad states ({}) ...", model.bad_states_initial.len(), bad_states_initial.len()); + debug!("Model:\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); + + match smt_solver { + #[rustfmt::skip] + SmtType::Generic => { + optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query) + }, + #[rustfmt::skip] + #[cfg(feature = "boolector")] + SmtType::Boolector => { + optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query) + }, + #[rustfmt::skip] + #[cfg(feature = "z3")] + SmtType::Z3 => { + optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query) + }, + } - let elapsed = reason( - model, - has_concrete_inputs, - input_values, - start, - mid, - prune, - &smt_solver, - timeout, - minimize); + let elapsed = now.elapsed(); if *time_budget < elapsed { end = mid - 1; - last_timeout = mid; debug!("Elapsed: {:#?}", elapsed); - } else if *time_budget > elapsed - && last_timeout > mid { + } else if *time_budget > elapsed { start = mid + 1; + + last_n = mid; + last_exec_time = elapsed; - *time_budget = *time_budget - elapsed; debug!("Elapsed: {:#?}", elapsed); } + } - if *time_budget == elapsed - || mid + 1 == last_timeout { - return mid; - } + (last_n, last_exec_time) +} - debug!("New steps: {} - {} ...", start, end); - debug!("Remaining time budget: {:#?} ...", time_budget); - } - panic!("No result during backwards reasoning") -} \ No newline at end of file +pub fn print_reasoning_horizon(model: &mut Model) { + let v: Option; + v = match &*model.bad_states_initial[0].borrow() { + Node::Bad { name, ..} => name.clone(), + _ => None + }; + + let bad_state = v.as_ref().expect("Bad state must have an unrolling depth"); + warn!("(Initial) Bad state '{}' is satisfiable.", bad_state); +} + +// +// Private Interface +// \ No newline at end of file diff --git a/src/unicorn/optimize.rs b/src/unicorn/optimize.rs index 58208d4d..b96937b9 100644 --- a/src/unicorn/optimize.rs +++ b/src/unicorn/optimize.rs @@ -744,43 +744,6 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> { } } - fn should_retain_bad_states(&mut self, bad_states: &Vec, use_smt: bool) -> bool { - debug!("bad_states_initial.len() = {}", bad_states.len()); - - let mut conds: Vec = Vec::new(); - - for bad_state in bad_states.iter() { - self.visit(bad_state); - - let v = &*bad_state.borrow(); - if let Node::Bad { cond, .. } = v { - conds.push(cond.clone()); - } - } - - if use_smt { - match self.smt_solver.solve_n(&conds) { - SMTSolution::Sat => { - // warn!( - // "A bad state '{}' is satisfiable within the last {} unrollings!", - // name.as_deref().unwrap_or("?"), - // conds.len() - // ); - return true; - } - SMTSolution::Unsat => { - // debug!( - // "Bad state '{}' is unsatisfiable , removing", - // name.as_deref().unwrap_or("?") - // ); - return false; - } - SMTSolution::Timeout => (), - } - } - true - } - fn should_retain_sequential(&mut self, sequential: &NodeRef) -> bool { if let Node::Next { state, next, .. } = &*sequential.borrow() { if let Node::State { init, name, .. } = &*state.borrow() { From fa39d571847bcf9b8e20258cfdebbd75651681f8 Mon Sep 17 00:00:00 2001 From: Daniel Kocher Date: Tue, 24 Jan 2023 17:54:09 +0100 Subject: [PATCH 17/19] feat: Draft of reasoning horizon for a give time budget in ms (exp. search + binary search) --- src/unicorn/horizon.rs | 165 +++++++++++++++++++---------------------- 1 file changed, 77 insertions(+), 88 deletions(-) diff --git a/src/unicorn/horizon.rs b/src/unicorn/horizon.rs index 0ea2229a..eca1f6e0 100644 --- a/src/unicorn/horizon.rs +++ b/src/unicorn/horizon.rs @@ -51,6 +51,7 @@ pub fn compute_reasoning_horizon( prev_n, n, prune, + stride, &smt_solver, timeout, minimize, @@ -61,6 +62,8 @@ pub fn compute_reasoning_horizon( exec_time += elapsed; if has_time_budget && time_budget.unwrap() < exec_time { + exec_time -= elapsed; + // TODO(2): Cf. TODO(1) let r = reason_backwards( &mut model.clone(), @@ -68,6 +71,7 @@ pub fn compute_reasoning_horizon( prev_n, n, prune, + stride, &smt_solver, timeout, minimize, @@ -76,7 +80,7 @@ pub fn compute_reasoning_horizon( &(time_budget.unwrap() - exec_time) ); - warn!("Depth [n={}] (in {:#?})", r.0, exec_time - elapsed + r.1); + warn!("Reasoning horizon: depth [n={}] (in {:#?}/{:#?})", r.0, exec_time + r.1, time_budget.unwrap()); break; } @@ -104,6 +108,7 @@ pub fn reason( start: usize, end: usize, prune: bool, + stride: bool, smt_solver: &SmtType, timeout: Option, minimize: bool, @@ -112,8 +117,6 @@ pub fn reason( ) -> (Duration, Vec) { let now = Instant::now(); - debug!("Model (initial):\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); - for m in start..end { unroll_model(model, m); @@ -122,119 +125,109 @@ pub fn reason( } } - debug!("Model (after unrolling):\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); - if prune { prune_model(model); } - debug!("Model (after pruning):\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); - let bad_states_initial = model.bad_states_initial.clone(); match smt_solver { #[rustfmt::skip] SmtType::Generic => { - optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query) + optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query, stride) }, #[rustfmt::skip] #[cfg(feature = "boolector")] SmtType::Boolector => { - optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query) + optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query, stride) }, #[rustfmt::skip] #[cfg(feature = "z3")] SmtType::Z3 => { - optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query) + optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query, stride) }, } - debug!("Model (after SMT solver query):\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); - (now.elapsed(), bad_states_initial) } -pub fn reason_backwards( - model: &mut Model, - bad_states_initial: &Vec, - prev_n: usize, - n: usize, - prune: bool, - smt_solver: &SmtType, - timeout: Option, - minimize: bool, - terminate_on_bad: bool, - one_query: bool, - time_budget: &Duration, -) -> (usize, Duration) { - // warn!("Used up time budget of {:#?} somwhere in between the last {} steps", solver_time_budget.map(|&ms| Duration::from_millis(ms)).unwrap(), n-prev_n); +// +// Private Interface +// - debug!("Model (before pruning):\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); +fn reason_backwards( + model: &mut Model, + bad_states_initial: &Vec, + prev_n: usize, + n: usize, + prune: bool, + stride: bool, + smt_solver: &SmtType, + timeout: Option, + minimize: bool, + terminate_on_bad: bool, + one_query: bool, + time_budget: &Duration, +) -> (usize, Duration) { + debug!("Backwards reasoning (binary search) for the last {} bad states ...", bad_states_initial.len()); - if prune { + if prune { prune_model(model) - } - - debug!("Model (after pruning):\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); + } - - debug!("Backwards reasoning (binary search) for the last {} bad states ...", bad_states_initial.len()); - - let mut start: usize = prev_n; - let mut end: usize = n; - - let mut last_n: usize = n; - let mut last_exec_time = Duration::from_millis(0); + let mut start: usize = prev_n; + let mut end: usize = n; + + let mut last_n: usize = n; + let mut last_exec_time = Duration::from_millis(0); - while start <= end { + while start <= end { let mid: usize = (start + end)/2; - - debug!("Try to fit remaining time budget {:#?} into {} steps ({} to {})...", time_budget, mid-prev_n, prev_n, mid); - - let now = Instant::now(); - - model.bad_states_initial = - bad_states_initial.clone()[(prev_n - (mid-prev_n)) * 10..].to_vec(); + let steps: usize = mid - prev_n; + + debug!("Trying to fit remaining time budget {:#?} into the last {} steps ({} to {}) ...", time_budget, steps, prev_n, mid); + + let now = Instant::now(); + + model.bad_states_initial = + bad_states_initial.clone()[(prev_n - steps) * 10..].to_vec(); + + match smt_solver { + #[rustfmt::skip] + SmtType::Generic => { + optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query, stride) + }, + #[rustfmt::skip] + #[cfg(feature = "boolector")] + SmtType::Boolector => { + optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query, stride) + }, + #[rustfmt::skip] + #[cfg(feature = "z3")] + SmtType::Z3 => { + optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query, stride) + }, + } + + let elapsed = now.elapsed(); + + if *time_budget < elapsed { + end = mid - 1; + debug!("Elapsed time for the last {} steps: {:#?}", steps, elapsed); + } else if *time_budget > elapsed { + start = mid + 1; + + last_n = mid; + last_exec_time = elapsed; - debug!("Calling SMT solver with the last {} bad states ({}) ...", model.bad_states_initial.len(), bad_states_initial.len()); - debug!("Model:\n - sequentials: {}\n - bad_states_sequential: {}\n - bad_states_initial: {}", model.sequentials.len(), model.bad_states_sequential.len(), model.bad_states_initial.len()); - - match smt_solver { - #[rustfmt::skip] - SmtType::Generic => { - optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query) - }, - #[rustfmt::skip] - #[cfg(feature = "boolector")] - SmtType::Boolector => { - optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query) - }, - #[rustfmt::skip] - #[cfg(feature = "z3")] - SmtType::Z3 => { - optimize_model_with_solver::(model, timeout, minimize, terminate_on_bad, one_query) - }, - } + debug!("Elapsed time for the last {} steps: {:#?}", steps, elapsed); + } + } - let elapsed = now.elapsed(); - - if *time_budget < elapsed { - end = mid - 1; - debug!("Elapsed: {:#?}", elapsed); - } else if *time_budget > elapsed { - start = mid + 1; - - last_n = mid; - last_exec_time = elapsed; - - debug!("Elapsed: {:#?}", elapsed); - } - } - - (last_n, last_exec_time) + (last_n, last_exec_time) } -pub fn print_reasoning_horizon(model: &mut Model) { +fn print_reasoning_horizon(model: &mut Model) { let v: Option; v = match &*model.bad_states_initial[0].borrow() { Node::Bad { name, ..} => name.clone(), @@ -243,8 +236,4 @@ pub fn print_reasoning_horizon(model: &mut Model) { let bad_state = v.as_ref().expect("Bad state must have an unrolling depth"); warn!("(Initial) Bad state '{}' is satisfiable.", bad_state); -} - -// -// Private Interface -// \ No newline at end of file +} \ No newline at end of file From 992b02bbca406f4ef214617124c2f96d6b54a801 Mon Sep 17 00:00:00 2001 From: Daniel Kocher Date: Tue, 24 Jan 2023 17:55:19 +0100 Subject: [PATCH 18/19] fix: Quick fix that respect the stride option when the SMT solver is called (i.e., panic only if stride is disabled) --- src/unicorn/optimize.rs | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/src/unicorn/optimize.rs b/src/unicorn/optimize.rs index b96937b9..d42ef112 100644 --- a/src/unicorn/optimize.rs +++ b/src/unicorn/optimize.rs @@ -18,6 +18,7 @@ pub fn optimize_model_with_solver( minimize: bool, terminate_on_bad: bool, one_query: bool, + stride: bool ) { debug!("Optimizing model using '{}' SMT solver ...", S::name()); debug!("Setting SMT solver timeout to {:?} per query ...", timeout); @@ -29,12 +30,13 @@ pub fn optimize_model_with_solver( minimize, terminate_on_bad, one_query, + stride ) } pub fn optimize_model_with_input(model: &mut Model, inputs: &mut Vec) { debug!("Optimizing model with {} concrete inputs ...", inputs.len()); - optimize_model_impl::(model, inputs, None, false, false, false); + optimize_model_impl::(model, inputs, None, false, false, false, false); } // @@ -48,6 +50,7 @@ fn optimize_model_impl( minimize: bool, terminate_on_bad: bool, one_query: bool, + stride: bool ) { let mut constant_folder = ConstantFolder::::new(inputs, timeout, minimize); model @@ -70,10 +73,15 @@ fn optimize_model_impl( .retain(|s| constant_folder.should_retain_bad_state(s, false, true)); if model.bad_states_initial.is_empty() { - panic!("No bad states happen"); + if !stride { + panic!("No bad states happen"); + } } else if model.bad_states_initial.len() == 1 { constant_folder.should_retain_bad_state(&model.bad_states_initial[0], true, true); - panic!("No bad states happen"); + + if !stride { + panic!("No bad states happen"); + } } else { let mut ored_bad_states = NodeRef::from(Node::Or { nid: u64::MAX, @@ -91,9 +99,13 @@ fn optimize_model_impl( }); } if !constant_folder.smt_solver.is_always_false(&ored_bad_states) { - panic!("bad states are satisfiable!") + if !stride { + panic!("bad states are satisfiable!") + } } else { - panic!("No bad state happen.") + if !stride { + panic!("No bad state happen.") + } } } } From ab2ef8fb39953d7e4439836071aaeef9006cfe54 Mon Sep 17 00:00:00 2001 From: Daniel Kocher Date: Mon, 27 Mar 2023 08:54:12 +0200 Subject: [PATCH 19/19] iter: Fix reasoning horizon functionality (deal with updated order of bad states) --- src/unicorn/horizon.rs | 60 +++++++++++++++++++++++++++--------------- 1 file changed, 39 insertions(+), 21 deletions(-) diff --git a/src/unicorn/horizon.rs b/src/unicorn/horizon.rs index eca1f6e0..cb6297d1 100644 --- a/src/unicorn/horizon.rs +++ b/src/unicorn/horizon.rs @@ -64,6 +64,8 @@ pub fn compute_reasoning_horizon( if has_time_budget && time_budget.unwrap() < exec_time { exec_time -= elapsed; + debug!("Time budget exceeded: {:#?} ({:#?}+{:#?}; elapsed time) / {:#?} (time budget)", exec_time+elapsed, exec_time, elapsed, time_budget.unwrap()); + // TODO(2): Cf. TODO(1) let r = reason_backwards( &mut model.clone(), @@ -77,10 +79,10 @@ pub fn compute_reasoning_horizon( minimize, terminate_on_bad, one_query, - &(time_budget.unwrap() - exec_time) + &mut(time_budget.unwrap() - exec_time) ); - warn!("Reasoning horizon: depth [n={}] (in {:#?}/{:#?})", r.0, exec_time + r.1, time_budget.unwrap()); + warn!("Reasoning horizon: depth [n={}] in {:#?} (elapsed time) / {:#?} (time budget)", prev_n + r.0, exec_time + r.1, time_budget.unwrap()); break; } @@ -167,7 +169,7 @@ fn reason_backwards( minimize: bool, terminate_on_bad: bool, one_query: bool, - time_budget: &Duration, + time_budget: &mut Duration, ) -> (usize, Duration) { debug!("Backwards reasoning (binary search) for the last {} bad states ...", bad_states_initial.len()); @@ -175,22 +177,22 @@ fn reason_backwards( prune_model(model) } - let mut start: usize = prev_n; - let mut end: usize = n; + let mut start: usize = 0; + let mut end: usize = n - prev_n; - let mut last_n: usize = n; - let mut last_exec_time = Duration::from_millis(0); + let mut exec_n: usize = end; + let mut exec_time = Duration::from_millis(0); - while start <= end { - let mid: usize = (start + end)/2; - let steps: usize = mid - prev_n; + let mut mid: usize = start + (end - start) / 2; + let mut prev_mid: usize; - debug!("Trying to fit remaining time budget {:#?} into the last {} steps ({} to {}) ...", time_budget, steps, prev_n, mid); + while start < end { + debug!("Trying to fit remaining time budget {:#?} into the last {} steps ({} to {}) ...", time_budget, mid, mid, end); let now = Instant::now(); model.bad_states_initial = - bad_states_initial.clone()[(prev_n - steps) * 10..].to_vec(); + bad_states_initial.clone()[mid * 10 .. end * 10].to_vec(); match smt_solver { #[rustfmt::skip] @@ -210,21 +212,37 @@ fn reason_backwards( } let elapsed = now.elapsed(); + + if *time_budget > elapsed { + end = mid; + + exec_time += elapsed; + *time_budget -= elapsed; - if *time_budget < elapsed { - end = mid - 1; - debug!("Elapsed time for the last {} steps: {:#?}", steps, elapsed); - } else if *time_budget > elapsed { - start = mid + 1; + debug!("Elapsed time for the last {} steps: {:#?}", mid, elapsed); + } else if *time_budget < elapsed { + start = mid; - last_n = mid; - last_exec_time = elapsed; + exec_n = mid; + exec_time = elapsed; - debug!("Elapsed time for the last {} steps: {:#?}", steps, elapsed); + debug!("Elapsed time for the last {} steps: {:#?}", mid, elapsed); } + + // since we will not find a perfectly fitting time budget (as is the case + // in a traditional binary search), we need an additional termination + // criterion to avoid endless loops: + // We terminate once the pivot does not change anymore. + prev_mid = mid; + mid = start + (end - start)/2; + + if prev_mid == mid { + break; + } + } - (last_n, last_exec_time) + (exec_n, exec_time) } fn print_reasoning_horizon(model: &mut Model) {