diff --git a/src/cli.rs b/src/cli.rs index 55b9c823..6fd604be 100644 --- a/src/cli.rs +++ b/src/cli.rs @@ -259,6 +259,13 @@ pub fn args() -> Command { .allow_hyphen_values(true) .num_args(1..) ) + .arg( + Arg::new("benchmark") + .help("Symbolicaly benchmark the model") + .long("benchmark") + .num_args(1) + .value_parser(value_parser!(u64)) + ) ) .subcommand( Command::new("qubot") diff --git a/src/main.rs b/src/main.rs index 9d9ef72a..1c89baab 100644 --- a/src/main.rs +++ b/src/main.rs @@ -19,9 +19,13 @@ use crate::unicorn::memory::replace_memory; use crate::unicorn::optimize::{optimize_model_with_input, optimize_model_with_solver}; use crate::unicorn::qubot::{InputEvaluator, Qubot}; use crate::unicorn::sat_solver::solve_bad_states; +#[cfg(feature = "boolector")] +use crate::unicorn::smt_solver::boolector_impl::*; use crate::unicorn::smt_solver::*; use crate::unicorn::unroller::{prune_model, renumber_model, unroll_model}; -use crate::unicorn::write_model; +use crate::unicorn::{write_model, Model}; +#[cfg(feature = "boolector")] +use boolector_solver::{SolverResult, BV}; use ::unicorn::disassemble::disassemble; use ::unicorn::emulate::EmulatorState; @@ -93,6 +97,7 @@ fn main() -> Result<()> { let emulate_model = is_beator && args.get_flag("emulate"); let arg0 = expect_arg::(args, "input-file")?; let extras = collect_arg_values(args, "extras"); + let benchmark_max_input = args.get_one::("benchmark").cloned(); let mut model = if !input_is_dimacs { let mut model = if !input_is_btor2 { @@ -158,6 +163,11 @@ fn main() -> Result<()> { None }; + // Test input limitation + if let (Some(max_input), Some(model)) = (benchmark_max_input, &model) { + run_symbolic_benchmark(model, max_input)?; + } + if compile_model { assert!(!input_is_btor2, "cannot compile arbitrary BTOR2"); assert!(!input_is_dimacs, "cannot compile arbitrary DIMACS"); @@ -294,6 +304,53 @@ fn main() -> Result<()> { } } +fn run_symbolic_benchmark(model: &Model, max_input_size: u64) -> Result<()> { + #[cfg(feature = "boolector")] + let mut smt_solver: BoolectorSolver = BoolectorSolver::new(None); + + for n in 0..=max_input_size { + println!("Finding bounds for input size: {n}"); + + // Create new constraint environment + smt_solver.solver.push(1); + + // Assume input size is <= n + let max_input_bv = BV::from_u64(smt_solver.solver.clone(), n, 64); + let counter_bv = smt_solver.translate(&model.read_counter).into_bv(); + + println!( + "Comparing {} <= {}", + counter_bv.as_binary_str().unwrap_or("NONE".to_string()), + max_input_bv.as_binary_str().unwrap_or("NONE".to_string()) + ); + + counter_bv.ulte(&max_input_bv).assert(); + + let result = smt_solver.solver.sat(); + match result { + SolverResult::Sat => { + println!("SAT") + } + SolverResult::Unsat => { + println!("UNSAT") + } + SolverResult::Unknown => { + println!("UNKNOWN") + } + } + + // TODO Find upper bound + + // TODO Find lower bound + + // TODO Add bound to the graph + + smt_solver.solver.pop(1); + } + + Ok(()) +} + fn init_logger(cli_log_level: LogLevel) -> Result<()> { let log_level_env_var = "MONSTER_LOG"; let log_style_env_var = "MONSTER_LOG_STYLE"; diff --git a/src/unicorn/btor2file_parser.rs b/src/unicorn/btor2file_parser.rs index 1827bb9b..2a8a684b 100644 --- a/src/unicorn/btor2file_parser.rs +++ b/src/unicorn/btor2file_parser.rs @@ -1,8 +1,10 @@ +use std::cell::RefCell; use std::collections::HashMap; use std::fs::File; use std::io::{self, BufRead}; use std::ops::Range; use std::path::Path; +use std::rc::Rc; #[cfg(feature = "gui")] use crate::guinea::MemoryData; @@ -29,6 +31,7 @@ pub fn parse_btor2_file(path: &Path) -> Model { heap_range: Range { start: 0, end: 0 }, stack_range: Range { start: 0, end: 0 }, memory_size: 0, + read_counter: Rc::new(RefCell::new(Node::Comment("dummy".to_string()))), } } @@ -62,6 +65,7 @@ pub fn parse_btor2_string(string: &str, data: &MemoryData) -> Model { heap_range: heap_start..heap_end, stack_range: stack_start..stack_end, memory_size: ByteSize::mib(data.memory_size).as_u64(), + read_counter: Rc::new(RefCell::new(Node::Comment("dummy".to_string()))), } } @@ -414,6 +418,7 @@ mod tests_btor2_parser { heap_range: Range { start: 0, end: 0 }, stack_range: Range { start: 0, end: 0 }, memory_size: 0, + read_counter: Rc::new(RefCell::new(Node::Comment("dummy".to_string()))), } } #[test] diff --git a/src/unicorn/builder.rs b/src/unicorn/builder.rs index 90cc6abe..521e919d 100644 --- a/src/unicorn/builder.rs +++ b/src/unicorn/builder.rs @@ -70,6 +70,7 @@ struct ModelBuilder { stack_range: Range, current_nid: Nid, pc: u64, + read_counter: NodeRef, } struct InEdge { @@ -111,7 +112,7 @@ impl ModelBuilder { division_flow: dummy_node.clone(), remainder_flow: dummy_node.clone(), access_flow: dummy_node.clone(), - ecall_flow: dummy_node, + ecall_flow: dummy_node.clone(), memory_size, max_heap_size: max_heap as u64 * size_of::() as u64, max_stack_size: max_stack as u64 * size_of::() as u64, @@ -120,6 +121,7 @@ impl ModelBuilder { stack_range: 0..0, current_nid: 0, pc: 0, + read_counter: dummy_node, } } @@ -133,6 +135,7 @@ impl ModelBuilder { heap_range: self.heap_range, stack_range: self.stack_range, memory_size: self.memory_size, + read_counter: self.read_counter, } } @@ -1184,6 +1187,25 @@ impl ModelBuilder { self.new_ite(activate, self.one_bit.clone(), flow, NodeType::Bit) } + // Generate global read counter which tracks how many bytes were read + fn generate_read_counter(&mut self, should_read_occur: NodeRef, how_much_to_read: NodeRef) { + let constant = self.new_const(1000000); + let read_counter = + self.new_state(Some(constant), "read-counter".to_string(), NodeType::Word); + + let possible_counter_value = self.new_add(how_much_to_read, read_counter.clone()); + let next_counter_value = self.new_ite( + should_read_occur, + possible_counter_value, + read_counter.clone(), + NodeType::Word, + ); + + self.new_next(read_counter.clone(), next_counter_value, NodeType::Word); + + self.read_counter = read_counter; + } + fn generate_model(&mut self, program: &Program, argv: &[String]) -> Result<()> { let data_section_start = program.data.address; let data_section_end = program.data.address + program.data.content.len() as u64; @@ -1350,17 +1372,23 @@ impl ModelBuilder { }) .context("Failed to decode instructions of program")?; + // System calls self.new_comment("syscalls".to_string()); self.current_nid = 40000000; let mut kernel_flow = self.kernel_mode.clone(); + let num_openat = self.new_const(SyscallId::Openat as u64); let is_openat = self.new_eq(self.reg_node(Register::A7), num_openat); + let num_read = self.new_const(SyscallId::Read as u64); let is_read = self.new_eq(self.reg_node(Register::A7), num_read); + let num_write = self.new_const(SyscallId::Write as u64); let is_write = self.new_eq(self.reg_node(Register::A7), num_write); + let num_exit = self.new_const(SyscallId::Exit as u64); let is_exit = self.new_eq(self.reg_node(Register::A7), num_exit); + let num_brk = self.new_const(SyscallId::Brk as u64); let is_brk = self.new_eq(self.reg_node(Register::A7), num_brk); @@ -1373,6 +1401,7 @@ impl ModelBuilder { NodeType::Bit, ); + // Read syscall self.current_nid = 42000000; let active_read = self.new_and_bit(self.ecall_flow.clone(), is_read.clone()); kernel_flow = self.new_ite( @@ -1391,50 +1420,58 @@ impl ModelBuilder { let read_const_8 = self.new_const(8); let read_full_word = self.new_ugte(read_remaining.clone(), read_const_8.clone()); let read_bytes = self.new_ite(read_full_word, read_const_8, read_remaining, NodeType::Word); + let read_input1 = self.new_input("1-byte-input".to_string(), NodeType::Input1Byte); let read_input2 = self.new_input("2-byte-input".to_string(), NodeType::Input2Byte); - let read_const_2 = self.new_const(2); - let read_bytes_eq_2 = self.new_eq(read_bytes.clone(), read_const_2); - let read_ite_2 = self.new_ite(read_bytes_eq_2, read_input2, read_input1, NodeType::Word); let read_input3 = self.new_input("3-byte-input".to_string(), NodeType::Input3Byte); - let read_const_3 = self.new_const(3); - let read_bytes_eq_3 = self.new_eq(read_bytes.clone(), read_const_3); - let read_ite_3 = self.new_ite(read_bytes_eq_3, read_input3, read_ite_2, NodeType::Word); let read_input4 = self.new_input("4-byte-input".to_string(), NodeType::Input4Byte); - let read_const_4 = self.new_const(4); - let read_bytes_eq_4 = self.new_eq(read_bytes.clone(), read_const_4); - let read_ite_4 = self.new_ite(read_bytes_eq_4, read_input4, read_ite_3, NodeType::Word); let read_input5 = self.new_input("5-byte-input".to_string(), NodeType::Input5Byte); - let read_const_5 = self.new_const(5); - let read_bytes_eq_5 = self.new_eq(read_bytes.clone(), read_const_5); - let read_ite_5 = self.new_ite(read_bytes_eq_5, read_input5, read_ite_4, NodeType::Word); let read_input6 = self.new_input("6-byte-input".to_string(), NodeType::Input6Byte); - let read_const_6 = self.new_const(6); - let read_bytes_eq_6 = self.new_eq(read_bytes.clone(), read_const_6); - let read_ite_6 = self.new_ite(read_bytes_eq_6, read_input6, read_ite_5, NodeType::Word); let read_input7 = self.new_input("7-byte-input".to_string(), NodeType::Input7Byte); - let read_const_7 = self.new_const(7); - let read_bytes_eq_7 = self.new_eq(read_bytes.clone(), read_const_7); - let read_ite_7 = self.new_ite(read_bytes_eq_7, read_input7, read_ite_6, NodeType::Word); let read_input8 = self.new_input("8-byte-input".to_string(), NodeType::Word); + + let read_const_2 = self.new_const(2); + let read_const_3 = self.new_const(3); + let read_const_4 = self.new_const(4); + let read_const_5 = self.new_const(5); + let read_const_6 = self.new_const(6); + let read_const_7 = self.new_const(7); let read_const_8 = self.new_const(8); + + let read_bytes_eq_2 = self.new_eq(read_bytes.clone(), read_const_2); + let read_bytes_eq_3 = self.new_eq(read_bytes.clone(), read_const_3); + let read_bytes_eq_4 = self.new_eq(read_bytes.clone(), read_const_4); + let read_bytes_eq_5 = self.new_eq(read_bytes.clone(), read_const_5); + let read_bytes_eq_6 = self.new_eq(read_bytes.clone(), read_const_6); + let read_bytes_eq_7 = self.new_eq(read_bytes.clone(), read_const_7); let read_bytes_eq_8 = self.new_eq(read_bytes.clone(), read_const_8); + + let read_ite_2 = self.new_ite(read_bytes_eq_2, read_input2, read_input1, NodeType::Word); + let read_ite_3 = self.new_ite(read_bytes_eq_3, read_input3, read_ite_2, NodeType::Word); + let read_ite_4 = self.new_ite(read_bytes_eq_4, read_input4, read_ite_3, NodeType::Word); + let read_ite_5 = self.new_ite(read_bytes_eq_5, read_input5, read_ite_4, NodeType::Word); + let read_ite_6 = self.new_ite(read_bytes_eq_6, read_input6, read_ite_5, NodeType::Word); + let read_ite_7 = self.new_ite(read_bytes_eq_7, read_input7, read_ite_6, NodeType::Word); let read_ite_8 = self.new_ite(read_bytes_eq_8, read_input8, read_ite_7, NodeType::Word); + let read_address = self.new_add(self.reg_node(Register::A1), self.reg_node(Register::A0)); let read_store = self.new_write(read_address, read_ite_8); + let read_more = self.new_ult(self.reg_node(Register::A0), self.reg_node(Register::A2)); let read_more = self.new_and_bit(is_read.clone(), read_more); let read_not_done = self.new_and_bit(self.kernel_mode.clone(), read_more); let read_not_zero = self.new_ugt(read_bytes.clone(), self.zero_word.clone()); let read_do_store = self.new_and_bit(read_not_done.clone(), read_not_zero); + let read_ite_mem = self.new_ite( - read_do_store, + read_do_store.clone(), read_store, self.memory_flow.clone(), NodeType::Memory, ); self.memory_flow = read_ite_mem; - let read_new_a0 = self.new_add(self.reg_node(Register::A0), read_bytes); + + let read_new_a0 = self.new_add(self.reg_node(Register::A0), read_bytes.clone()); let read_ite_a0 = self.new_ite( read_not_done.clone(), read_new_a0, @@ -1449,6 +1486,8 @@ impl ModelBuilder { NodeType::Bit, ); + self.generate_read_counter(read_do_store, read_bytes); + self.current_nid = 45000000; let active_brk = self.new_and_bit(self.ecall_flow.clone(), is_brk.clone()); let brk_init = self.new_const(self.heap_range.start); diff --git a/src/unicorn/mod.rs b/src/unicorn/mod.rs index a10ac26c..606a00c9 100644 --- a/src/unicorn/mod.rs +++ b/src/unicorn/mod.rs @@ -197,6 +197,7 @@ pub struct Model { pub heap_range: Range, pub stack_range: Range, pub memory_size: u64, + pub read_counter: NodeRef, } #[derive(Clone, Debug)] diff --git a/src/unicorn/optimize.rs b/src/unicorn/optimize.rs index 3b1ae872..4a03267c 100644 --- a/src/unicorn/optimize.rs +++ b/src/unicorn/optimize.rs @@ -737,18 +737,18 @@ impl<'a, S: SMTSolver> ConstantFolder<'a, S> { match self.smt_solver.solve(cond) { SMTSolution::Sat => { warn!( - "Bad state '{}' is satisfiable!", + "3Bad state '{}' is satisfiable!", name.as_deref().unwrap_or("?") ); if terminate_on_bad { // TODO: Change this to use return Result<> instead of panic! - panic!("Bad state satisfiable"); + panic!("4Bad state satisfiable"); } return true; } SMTSolution::Unsat => { debug!( - "Bad state '{}' is unsatisfiable, removing", + "5Bad state '{}' is unsatisfiable, removing", name.as_deref().unwrap_or("?") ); return false; diff --git a/src/unicorn/sat_solver.rs b/src/unicorn/sat_solver.rs index 6c97ef2b..e42de947 100644 --- a/src/unicorn/sat_solver.rs +++ b/src/unicorn/sat_solver.rs @@ -72,7 +72,7 @@ fn process_single_bad_state( match solution { SATSolution::Sat => { warn!( - "Bad state '{}' is satisfiable ({})!", + "1Bad state '{}' is satisfiable ({})!", name.as_deref().unwrap_or("?"), S::name() ); @@ -82,7 +82,7 @@ fn process_single_bad_state( } SATSolution::Unsat => { debug!( - "Bad state '{}' is unsatisfiable ({}).", + "2Bad state '{}' is unsatisfiable ({}).", name.as_deref().unwrap_or("?"), S::name() ); diff --git a/src/unicorn/smt_solver.rs b/src/unicorn/smt_solver.rs index 56fd3ffc..5cc3bdc6 100644 --- a/src/unicorn/smt_solver.rs +++ b/src/unicorn/smt_solver.rs @@ -79,13 +79,13 @@ pub mod boolector_impl { type BitVectorRef = BV>; #[derive(Clone)] - enum BoolectorValue { + pub enum BoolectorValue { BitVector(BitVectorRef), Array(ArrayRef), } pub struct BoolectorSolver { - solver: Rc, + pub solver: Rc, mapping: HashMap, } @@ -140,6 +140,7 @@ pub mod boolector_impl { SolverResult::Unknown => SMTSolution::Timeout, }; self.solver.pop(1); + if solution == SMTSolution::Timeout { debug!("Query timeout was reached by Boolector"); } @@ -157,7 +158,7 @@ pub mod boolector_impl { } #[rustfmt::skip] - fn translate(&mut self, node: &NodeRef) -> BoolectorValue { + pub fn translate(&mut self, node: &NodeRef) -> BoolectorValue { match &*node.borrow() { Node::Const { sort, imm, .. } => { let width = sort.bitsize() as u32; @@ -292,7 +293,7 @@ pub mod boolector_impl { } impl BoolectorValue { - fn into_bv(self) -> BitVectorRef { + pub fn into_bv(self) -> BitVectorRef { match self { BoolectorValue::BitVector(x) => x, _ => panic!("expected bit-vector"),