From b228716c7713039ea126b2d162c4a71238305dad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Christian=20M=C3=B6sl?= Date: Mon, 22 Feb 2021 21:46:19 +0100 Subject: [PATCH] refactor: Create Formula abstraction and create engine module --- .github/workflows/test.yml | 19 +- Cargo.lock | 51 ++-- Cargo.toml | 1 + src/cli.rs | 6 +- src/{ => engine}/bug.rs | 3 +- src/{engine.rs => engine/mod.rs} | 127 +++------ src/{ => engine}/symbolic_state.rs | 400 ++++++++++++++--------------- src/lib.rs | 74 +++++- src/main.rs | 52 ++-- src/solver/boolector.rs | 93 ++++--- src/solver/external.rs | 40 ++- src/solver/mod.rs | 124 +++++++-- src/solver/monster.rs | 261 ++++++++++--------- src/solver/z3.rs | 43 ++-- tests/common.rs | 10 +- tests/engine.rs | 83 ++++-- 16 files changed, 774 insertions(+), 613 deletions(-) rename src/{ => engine}/bug.rs (98%) rename src/{engine.rs => engine/mod.rs} (90%) rename src/{ => engine}/symbolic_state.rs (53%) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 89212d1b..68dcaefd 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -49,14 +49,20 @@ jobs: if: ${{ contains(matrix.os, 'windows') }} # MinGw64 and Git is already installed # https://github.com/actions/virtual-environments/blob/main/images/win/Windows2019-Readme.md - run: choco install make -y + run: | + choco install make -y + echo "TEMP=$env:USERPROFILE\AppData\Local\Temp" >> $env:GITHUB_ENV + echo "TMP=$env:USERPROFILE\AppData\Local\Temp" >> $env:GITHUB_ENV - name: Cache Cargo Dependencies uses: actions/cache@v2 env: cache-name: cache-cargo-dependencies # disable cache for scheduled builds - if: ${{ github.event_name != 'schedule' }} + # Unfortunately MacOs in combination with the Github Cache action has a bug: + # https://github.com/actions/virtual-environments/issues/2619 + # This is a workaround to fix curroption of cached cargo dependencies + if: ${{ github.event_name != 'schedule' && !contains(matrix.os, 'macos') }} with: # cargo cache files are stored in `~/.cargo` on Linux/macOS # source for paths: https://doc.rust-lang.org/cargo/guide/cargo-home.html#caching-the-cargo-home-in-ci @@ -108,12 +114,3 @@ jobs: with: command: test args: --features ${{ matrix.features }} --locked - - # Unfortunately MacOs in combination with the Github Cache action has a bug: - # https://github.com/actions/virtual-environments/issues/2619 - # This is a workaround to fix curroption of cached cargo dependencies - - name: Cache Sync - if: ${{ contains(matrix.os, 'macos') }} - run: sleep 10 - - diff --git a/Cargo.lock b/Cargo.lock index 07930481..4cd7215f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -137,6 +137,26 @@ dependencies = [ "cc", ] +[[package]] +name = "const_format" +version = "0.2.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c0412fd9e3c921f868af82a0097da41c250087e513786858b9e6b6055f8ed300" +dependencies = [ + "const_format_proc_macros", +] + +[[package]] +name = "const_format_proc_macros" +version = "0.2.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8df496e1bbc93814d728a8036ff054cd95830afe9cf2275c9326688c02eff936" +dependencies = [ + "proc-macro2", + "quote", + "unicode-xid", +] + [[package]] name = "copy_dir" version = "0.1.2" @@ -229,14 +249,14 @@ checksum = "37ab347416e802de484e4d03c7316c48f1ecb56574dfd4a46a80f173ce1de04d" [[package]] name = "generator" -version = "0.6.23" +version = "0.6.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8cdc09201b2e8ca1b19290cf7e65de2246b8e91fb6874279722189c4de7b94dc" +checksum = "a9fed24fd1e18827652b4d55652899a1e9da8e54d91624dc3437a5bc3a9f9a9c" dependencies = [ "cc", "libc", "log", - "rustc_version", + "rustversion", "winapi 0.3.9", ] @@ -387,6 +407,7 @@ dependencies = [ "bytesize", "cargo-husky", "clap", + "const_format", "divisors", "env_logger", "itertools", @@ -676,13 +697,10 @@ dependencies = [ ] [[package]] -name = "rustc_version" -version = "0.2.3" +name = "rustversion" +version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "138e3e0acb6c9fb258b19b67cb8abd63c00679d2851805ea151465464fe9030a" -dependencies = [ - "semver", -] +checksum = "cb5d2a036dc6d2d8fd16fde3498b04306e29bd193bf306a57427019b823d5acd" [[package]] name = "scoped-tls" @@ -716,21 +734,6 @@ dependencies = [ "syn", ] -[[package]] -name = "semver" -version = "0.9.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1d7eb9ef2c18661902cc47e535f9bc51b78acd254da71d375c2f6720d9a40403" -dependencies = [ - "semver-parser", -] - -[[package]] -name = "semver-parser" -version = "0.7.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "388a1df253eca08550bef6c72392cfe7c30914bf41df5269b68cbd6ff8f570a3" - [[package]] name = "strsim" version = "0.10.0" diff --git a/Cargo.toml b/Cargo.toml index b429cebb..cb93d236 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -38,6 +38,7 @@ itertools = "~0.9.0" anyhow = "~1.0.34" thiserror = "~1.0.22" divisors = "~0.2.1" +const_format = "~0.2.13" boolector = { version = "~0.4.2", features = ["vendor-lgl"], optional = true } z3 = { version = "~0.7.1", features = ["static-link-z3"], optional = true } diff --git a/src/cli.rs b/src/cli.rs index 5c6becb1..087647e0 100644 --- a/src/cli.rs +++ b/src/cli.rs @@ -1,5 +1,7 @@ +use crate::engine::{DEFAULT_MAX_EXECUTION_DEPTH, DEFAULT_MEMORY_SIZE}; use anyhow::Result; use clap::{crate_authors, crate_description, crate_version, App, AppSettings, Arg, ArgMatches}; +use const_format::formatcp; pub const LOGGING_LEVELS: [&str; 5] = ["trace", "debug", "info", "warn", "error"]; pub const SOLVER: [&str; 4] = ["monster", "boolector", "z3", "external"]; @@ -107,7 +109,7 @@ pub fn args() -> App<'static> { .long("execution-depth") .takes_value(true) .value_name("NUMBER") - .default_value("1000") + .default_value(formatcp!("{}", DEFAULT_MAX_EXECUTION_DEPTH)) .validator(is_u64), ) .arg( @@ -117,7 +119,7 @@ pub fn args() -> App<'static> { .long("memory") .takes_value(true) .value_name("NUMBER") - .default_value("1") + .default_value(formatcp!("{}", DEFAULT_MEMORY_SIZE.0 / bytesize::MB)) .validator(is_valid_memory_size), ), ) diff --git a/src/bug.rs b/src/engine/bug.rs similarity index 98% rename from src/bug.rs rename to src/engine/bug.rs index 250717cf..daee8da5 100644 --- a/src/bug.rs +++ b/src/engine/bug.rs @@ -1,7 +1,6 @@ use crate::{ engine::{instruction_to_str, Value}, - solver::BitVector, - symbolic_state::BVOperator, + solver::{BVOperator, BitVector}, }; use riscu::Instruction; use std::fmt; diff --git a/src/engine.rs b/src/engine/mod.rs similarity index 90% rename from src/engine.rs rename to src/engine/mod.rs index 7b5ebb9e..6504bd79 100644 --- a/src/engine.rs +++ b/src/engine/mod.rs @@ -1,28 +1,30 @@ +pub mod bug; +pub mod symbolic_state; + +pub use bug::Bug; + +use self::{ + bug::BasicInfo, + symbolic_state::{Query, SymbolicState, SymbolicValue}, +}; use crate::{ - bug::{BasicInfo, Bug}, - path_exploration::{ExplorationStrategy, ShortestPathStrategy}, - solver::{ExternalSolver, MonsterSolver, Solver, SolverError}, - symbolic_state::{BVOperator, Query, SymbolId, SymbolicState}, + path_exploration::ExplorationStrategy, + solver::{BVOperator, Solver, SolverError}, }; use byteorder::{ByteOrder, LittleEndian}; use bytesize::ByteSize; use log::{debug, trace}; use riscu::{ - decode, load_object_file, types::*, DecodingError, Instruction, Program, ProgramSegment, - Register, INSTRUCTION_SIZE as INSTR_SIZE, + decode, types::*, DecodingError, Instruction, Program, ProgramSegment, Register, + INSTRUCTION_SIZE as INSTR_SIZE, }; -use std::{fmt, mem::size_of, path::Path, rc::Rc}; +use std::{fmt, mem::size_of}; use thiserror::Error; -#[cfg(feature = "boolector-solver")] -use crate::solver::Boolector; - -#[cfg(feature = "z3-solver")] -use crate::solver::Z3; - const INSTRUCTION_SIZE: u64 = INSTR_SIZE as u64; +pub const DEFAULT_MEMORY_SIZE: ByteSize = ByteSize(bytesize::MB); +pub const DEFAULT_MAX_EXECUTION_DEPTH: u64 = 1000; -#[allow(dead_code)] pub enum SyscallId { Exit = 93, Read = 63, @@ -30,74 +32,25 @@ pub enum SyscallId { Openat = 56, Brk = 214, } -#[derive(Copy, Clone)] -pub enum Backend { - Monster, - External, - - #[cfg(feature = "boolector-solver")] - Boolector, - #[cfg(feature = "z3-solver")] - Z3, +pub struct EngineOptions { + pub memory_size: ByteSize, + pub max_exection_depth: u64, } -pub fn execute

( - input: P, - with: Backend, - max_exection_depth: u64, - memory_size: ByteSize, -) -> Result, EngineError> -where - P: AsRef, -{ - let program = load_object_file(input).map_err(|e| { - EngineError::IoError(anyhow::Error::new(e).context("Failed to load object file")) - })?; - - let strategy = ShortestPathStrategy::compute_for(&program).map_err(EngineError::IoError)?; - - match with { - Backend::Monster => { - create_and_run::<_, MonsterSolver>(&program, &strategy, max_exection_depth, memory_size) +impl Default for EngineOptions { + fn default() -> EngineOptions { + EngineOptions { + memory_size: DEFAULT_MEMORY_SIZE, + max_exection_depth: DEFAULT_MAX_EXECUTION_DEPTH, } - #[cfg(feature = "boolector-solver")] - Backend::Boolector => { - create_and_run::<_, Boolector>(&program, &strategy, max_exection_depth, memory_size) - } - #[cfg(feature = "z3-solver")] - Backend::Z3 => { - create_and_run::<_, Z3>(&program, &strategy, max_exection_depth, memory_size) - } - Backend::External => create_and_run::<_, ExternalSolver>( - &program, - &strategy, - max_exection_depth, - memory_size, - ), } } -fn create_and_run( - program: &Program, - strategy: &E, - max_exection_depth: u64, - memory_size: ByteSize, -) -> Result, EngineError> -where - E: ExplorationStrategy, - S: Solver + Default, -{ - let solver = Rc::new(S::default()); - let state = Box::new(SymbolicState::new(solver)); - - Engine::new(memory_size, max_exection_depth, &program, strategy, state).run() -} - #[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)] pub enum Value { Concrete(u64), - Symbolic(SymbolId), + Symbolic(SymbolicValue), Uninitialized, } @@ -134,7 +87,7 @@ where E: ExplorationStrategy, S: Solver, { - symbolic_state: Box>, + symbolic_state: Box>, program_break: u64, pc: u64, regs: [Value; 32], @@ -151,17 +104,12 @@ where S: Solver, { // creates a machine state with a specific memory size - pub fn new( - memory_size: ByteSize, - max_exection_depth: u64, - program: &Program, - strategy: &'a E, - symbolic_state: Box>, - ) -> Self { + pub fn new(program: &Program, options: &EngineOptions, strategy: &'a E, solver: &'a S) -> Self { let mut regs = [Value::Uninitialized; 32]; - let mut memory = vec![Value::Uninitialized; memory_size.as_u64() as usize / 8]; + let memory_size = options.memory_size.as_u64(); + let mut memory = vec![Value::Uninitialized; memory_size as usize / 8]; - let sp = memory_size.as_u64() - 8; + let sp = memory_size - 8; regs[Register::Sp as usize] = Value::Concrete(sp); regs[Register::Zero as usize] = Value::Concrete(0); @@ -176,6 +124,8 @@ where let program_break = program.data.address + program.data.content.len() as u64; + let symbolic_state = Box::new(SymbolicState::new(solver)); + debug!( "initializing new execution context with {} of main memory", memory_size @@ -203,7 +153,7 @@ where memory, strategy, execution_depth: 0, - max_exection_depth, + max_exection_depth: options.max_exection_depth, is_running: false, } } @@ -484,7 +434,12 @@ where } } - fn bytewise_combine(&mut self, old: Value, n_lower_bytes: u32, new_idx: SymbolId) -> SymbolId { + fn bytewise_combine( + &mut self, + old: Value, + n_lower_bytes: u32, + new_idx: SymbolicValue, + ) -> SymbolicValue { let bits_in_a_byte = 8; let low_shift_factor = 2_u64.pow(n_lower_bytes * bits_in_a_byte); let high_shift_factor = @@ -613,8 +568,8 @@ where &mut self, true_branch: u64, false_branch: u64, - lhs: SymbolId, - rhs: SymbolId, + lhs: SymbolicValue, + rhs: SymbolicValue, ) -> Result, EngineError> { let memory_snapshot = self.memory.clone(); let regs_snapshot = self.regs; diff --git a/src/symbolic_state.rs b/src/engine/symbolic_state.rs similarity index 53% rename from src/symbolic_state.rs rename to src/engine/symbolic_state.rs index 2ce900f0..3d5ab768 100644 --- a/src/symbolic_state.rs +++ b/src/engine/symbolic_state.rs @@ -1,86 +1,26 @@ -use crate::{ - bug::Witness, - solver::{BitVector, Solver, SolverError}, +use super::bug::Witness; +use crate::solver::{ + BVOperator, BitVector, Formula, FormulaVisitor, OperandSide, Solver, SolverError, Symbol, + SymbolId, }; use log::{debug, trace, Level}; pub use petgraph::graph::{EdgeIndex, NodeIndex}; -use petgraph::{Direction, Graph}; +use petgraph::visit::EdgeRef; +use petgraph::{ + graph::{Neighbors, NodeIndices}, + Direction, +}; use riscu::Instruction; -use std::{collections::HashMap, fmt, rc::Rc}; - -#[derive(Clone, Debug, Copy, Eq, Hash, PartialEq)] -pub enum OperandSide { - Lhs, - Rhs, -} - -impl OperandSide { - #[allow(dead_code)] - pub fn other(&self) -> Self { - match self { - OperandSide::Lhs => OperandSide::Rhs, - OperandSide::Rhs => OperandSide::Lhs, - } - } -} - -#[derive(Debug, Copy, Clone, Hash, Eq, PartialEq)] -pub enum BVOperator { - Add, - Sub, - Mul, - Divu, - Sltu, - Remu, - Not, - Equals, - BitwiseAnd, -} - -impl BVOperator { - pub fn is_unary(&self) -> bool { - *self == BVOperator::Not - } - pub fn is_binary(&self) -> bool { - !self.is_unary() - } -} - -impl fmt::Display for BVOperator { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - write!( - f, - "{}", - match self { - BVOperator::Add => "+", - BVOperator::Sub => "-", - BVOperator::Mul => "*", - BVOperator::Divu => "/", - BVOperator::Not => "!", - BVOperator::Remu => "%", - BVOperator::Equals => "=", - BVOperator::BitwiseAnd => "&", - BVOperator::Sltu => "<", - } - ) - } -} +use std::{collections::HashMap, ops::Index}; pub enum Query { - Equals((SymbolId, u64)), - NotEquals((SymbolId, u64)), + Equals((SymbolicValue, u64)), + NotEquals((SymbolicValue, u64)), Reachable, } -#[derive(Clone, Debug, Eq, Hash, PartialEq)] -pub enum Node { - Constant(u64), - Input(String), - Operator(BVOperator), -} - -pub type Formula = Graph; -pub type SymbolId = NodeIndex; +pub type SymbolicValue = NodeIndex; +pub type DataFlowGraph = petgraph::Graph; fn instruction_to_bv_operator(instruction: Instruction) -> BVOperator { match instruction { @@ -94,35 +34,17 @@ fn instruction_to_bv_operator(instruction: Instruction) -> BVOperator { } } -pub fn get_operands(graph: &Formula, sym: SymbolId) -> (SymbolId, Option) { - let mut iter = graph.neighbors_directed(sym, Direction::Incoming).detach(); - - let lhs = iter - .next(graph) - .expect("get_operands() should not be called on operators without operands") - .1; - - let rhs = iter.next(graph).map(|n| n.1); - - assert!( - iter.next(graph) == None, - "operators with arity 1 or 2 are supported only" - ); - - (lhs, rhs) -} - #[derive(Debug)] -pub struct SymbolicState +pub struct SymbolicState<'a, S> where S: Solver, { - data_flow: Graph, - path_condition: Option, - solver: Rc, + data_flow: DataFlowGraph, + path_condition: Option, + solver: &'a S, } -impl Clone for SymbolicState +impl<'a, S> Clone for SymbolicState<'a, S> where S: Solver, { @@ -130,25 +52,25 @@ where Self { data_flow: self.data_flow.clone(), path_condition: self.path_condition, - solver: self.solver.clone(), + solver: self.solver, } } } -impl<'a, S> SymbolicState +impl<'a, S> SymbolicState<'a, S> where S: Solver, { - pub fn new(solver: Rc) -> Self { + pub fn new(solver: &'a S) -> Self { Self { - data_flow: Graph::new(), + data_flow: DataFlowGraph::new(), path_condition: None, solver, } } - pub fn create_const(&mut self, value: u64) -> SymbolId { - let constant = Node::Constant(value); + pub fn create_const(&mut self, value: u64) -> SymbolicValue { + let constant = Symbol::Constant(BitVector(value)); let i = self.data_flow.add_node(constant); @@ -160,9 +82,9 @@ where pub fn create_instruction( &mut self, instruction: Instruction, - lhs: SymbolId, - rhs: SymbolId, - ) -> SymbolId { + lhs: SymbolicValue, + rhs: SymbolicValue, + ) -> SymbolicValue { let op = instruction_to_bv_operator(instruction); let root = self.create_operator(op, lhs, rhs); @@ -170,7 +92,7 @@ where // constrain divisor to be not zero, // as division by zero is allowed in SMT bit-vector formulas if matches!(op, BVOperator::Divu) - && matches!(self.data_flow[rhs], Node::Operator(_) | Node::Input(_)) + && matches!(self.data_flow[rhs], Symbol::Operator(_) | Symbol::Input(_)) { let zero = self.create_const(0); let negated_condition = self.create_operator(BVOperator::Equals, rhs, zero); @@ -182,15 +104,20 @@ where root } - pub fn create_operator(&mut self, op: BVOperator, lhs: SymbolId, rhs: SymbolId) -> SymbolId { + pub fn create_operator( + &mut self, + op: BVOperator, + lhs: SymbolicValue, + rhs: SymbolicValue, + ) -> SymbolicValue { assert!(op.is_binary(), "has to be a binary operator"); - let n = Node::Operator(op); + let n = Symbol::Operator(op); let n_idx = self.data_flow.add_node(n); assert!(!( - matches!(self.data_flow[lhs], Node::Constant(_)) - && matches!(self.data_flow[rhs], Node::Constant(_)) + matches!(self.data_flow[lhs], Symbol::Constant(_)) + && matches!(self.data_flow[rhs], Symbol::Constant(_)) ), "every operand has to be derived from an input or has to be an (already folded) constant" ); @@ -208,18 +135,18 @@ where n_idx } - fn create_unary_operator(&mut self, op: BVOperator, v: SymbolId) -> SymbolId { + fn create_unary_operator(&mut self, op: BVOperator, v: SymbolicValue) -> SymbolicValue { assert!(op.is_unary(), "has to be a unary operator"); - let op_id = self.data_flow.add_node(Node::Operator(op)); + let op_id = self.data_flow.add_node(Symbol::Operator(op)); self.data_flow.add_edge(v, op_id, OperandSide::Lhs); op_id } - pub fn create_input(&mut self, name: &str) -> SymbolId { - let node = Node::Input(String::from(name)); + pub fn create_input(&mut self, name: &str) -> SymbolicValue { + let node = Symbol::Input(String::from(name)); let idx = self.data_flow.add_node(node); @@ -228,7 +155,12 @@ where idx } - pub fn create_beq_path_condition(&mut self, decision: bool, lhs: SymbolId, rhs: SymbolId) { + pub fn create_beq_path_condition( + &mut self, + decision: bool, + lhs: SymbolicValue, + rhs: SymbolicValue, + ) { let mut pc_idx = self.create_operator(BVOperator::Equals, lhs, rhs); if !decision { @@ -238,7 +170,7 @@ where self.add_path_condition(pc_idx) } - fn add_path_condition(&mut self, condition: SymbolId) { + fn add_path_condition(&mut self, condition: SymbolicValue) { let new_condition = if let Some(old_condition) = self.path_condition { self.create_operator(BVOperator::BitwiseAnd, old_condition, condition) } else { @@ -264,16 +196,18 @@ where } }; + let formula = FormulaView::new(&self.data_flow, root); + if log::log_enabled!(Level::Debug) { debug!("query to solve:"); - let root_idx = self.print_recursive(root); + let root = formula.print_recursive(); - debug!("assert x{} is 1", root_idx.index()); + debug!("assert x{} is 1", root); } - let result = match self.solver.solve(&self.data_flow, root) { - Ok(Some(ref assignment)) => Ok(Some(self.build_witness(root, assignment))), + let result = match self.solver.solve(&formula) { + Ok(Some(ref assignment)) => Ok(Some(formula.build_witness(assignment))), Ok(None) => Ok(None), Err(e) => Err(e), }; @@ -290,14 +224,14 @@ where fn append_path_condition( &mut self, - r: NodeIndex, - mut ns: Vec, + r: SymbolicValue, + mut ns: Vec, mut es: Vec, - ) -> (NodeIndex, Vec, Vec) { + ) -> (SymbolicValue, Vec, Vec) { if let Some(pc_idx) = self.path_condition { let con_idx = self .data_flow - .add_node(Node::Operator(BVOperator::BitwiseAnd)); + .add_node(Symbol::Operator(BVOperator::BitwiseAnd)); let (con_edge_idx1, con_edge_idx2) = self.connect_operator(pc_idx, r, con_idx); ns.push(con_idx); @@ -310,12 +244,17 @@ where } } - fn prepare_query(&mut self, query: Query) -> (NodeIndex, Vec, Vec) { + fn prepare_query( + &mut self, + query: Query, + ) -> (SymbolicValue, Vec, Vec) { match query { Query::Equals((sym, c)) | Query::NotEquals((sym, c)) => { - let root_idx = self.data_flow.add_node(Node::Operator(BVOperator::Equals)); + let root_idx = self + .data_flow + .add_node(Symbol::Operator(BVOperator::Equals)); - let const_idx = self.data_flow.add_node(Node::Constant(c)); + let const_idx = self.data_flow.add_node(Symbol::Constant(BitVector(c))); let const_edge_idx = self .data_flow .add_edge(const_idx, root_idx, OperandSide::Lhs); @@ -323,7 +262,7 @@ where let sym_edge_idx = self.data_flow.add_edge(sym, root_idx, OperandSide::Rhs); if let Query::NotEquals(_) = query { - let not_idx = self.data_flow.add_node(Node::Operator(BVOperator::Not)); + let not_idx = self.data_flow.add_node(Symbol::Operator(BVOperator::Not)); let not_edge_idx = self.data_flow.add_edge(root_idx, not_idx, OperandSide::Lhs); self.append_path_condition( @@ -345,9 +284,9 @@ where fn connect_operator( &mut self, - lhs: SymbolId, - rhs: SymbolId, - op: SymbolId, + lhs: SymbolicValue, + rhs: SymbolicValue, + op: SymbolicValue, ) -> (EdgeIndex, EdgeIndex) { // assert: right hand side edge has to be inserted first // solvers depend on edge insertion order!!! @@ -357,27 +296,38 @@ where ) } - fn print_recursive(&self, root: NodeIndex) -> NodeIndex { - let mut visited = HashMap::::new(); - let mut printer = Printer {}; - - traverse(&self.data_flow, root, &mut visited, &mut printer) - } - fn build_trivial_witness(&self) -> Witness { let mut witness = Witness::new(); self.data_flow.node_indices().for_each(|idx| { - if let Node::Input(name) = &self.data_flow[idx] { + if let Symbol::Input(name) = &self.data_flow[idx] { witness.add_variable(name.as_str(), BitVector(0)); } }); witness } +} + +pub struct FormulaView<'a> { + data_flow: &'a DataFlowGraph, + root: SymbolicValue, +} + +impl<'a> FormulaView<'a> { + pub fn new(data_flow: &'a DataFlowGraph, root: SymbolicValue) -> Self { + Self { data_flow, root } + } + + pub fn print_recursive(&self) -> SymbolId { + let mut visited = HashMap::::new(); + let mut printer = Printer {}; + + self.traverse(self.root(), &mut visited, &mut printer) + } - fn build_witness(&self, root: NodeIndex, assignment: &HashMap) -> Witness { - let mut visited = HashMap::::new(); + fn build_witness(&self, assignment: &HashMap) -> Witness { + let mut visited = HashMap::::new(); let mut witness = Witness::new(); let mut builder = WitnessBuilder { @@ -385,95 +335,145 @@ where assignment, }; - traverse(&self.data_flow, root, &mut visited, &mut builder); + self.traverse(self.root(), &mut visited, &mut builder); witness } } -pub fn traverse( - formula: &Formula, - n: SymbolId, - visit_map: &mut HashMap, - v: &mut V, -) -> R -where - V: FormulaVisitor, - R: Clone, -{ - if let Some(result) = visit_map.get(&n) { - return (*result).clone(); +impl<'a> Index for FormulaView<'a> { + type Output = Symbol; + + fn index(&self, idx: SymbolId) -> &Self::Output { + &self.data_flow[NodeIndex::new(idx)] } +} - let result = match &formula[n] { - Node::Operator(op) => { - let mut operands = formula.neighbors_directed(n, Direction::Incoming).detach(); +impl<'a> Formula for FormulaView<'a> { + type DependencyIter = std::iter::Map, fn(NodeIndex) -> usize>; + type SymbolIdsIter = std::iter::Map usize>; - if op.is_unary() { - let x = operands - .next(formula) - .expect("every unary operator must have 1 operand") - .1; + fn root(&self) -> SymbolId { + self.root.index() + } - let x = traverse(formula, x, visit_map, v); + fn operands(&self, sym: SymbolId) -> (SymbolId, Option) { + let mut iter = self + .data_flow + .neighbors_directed(NodeIndex::new(sym), Direction::Incoming) + .detach(); - v.unary(n, *op, x) - } else { - let lhs = operands - .next(formula) - .expect("every binary operator must have an lhs operand") - .1; + let lhs = iter + .next(self.data_flow) + .expect("get_operands() should not be called on operators without operands") + .1 + .index(); - let rhs = operands - .next(formula) - .expect("every binary operator must have an rhs operand") - .1; + let rhs = iter.next(self.data_flow).map(|n| n.1.index()); - let lhs = traverse(formula, lhs, visit_map, v); - let rhs = traverse(formula, rhs, visit_map, v); + assert!( + iter.next(self.data_flow) == None, + "operators with arity 1 or 2 are supported only" + ); - v.binary(n, *op, lhs, rhs) - } + (lhs, rhs) + } + + fn operand(&self, sym: SymbolId) -> SymbolId { + self.data_flow + .edges_directed(NodeIndex::new(sym), Direction::Incoming) + .next() + .expect("every unary operator must have an operand") + .source() + .index() + } + + fn dependencies(&self, sym: SymbolId) -> Self::DependencyIter { + self.data_flow + .neighbors_directed(NodeIndex::new(sym), Direction::Outgoing) + .map(|idx| idx.index()) + } + + fn symbol_ids(&self) -> Self::SymbolIdsIter { + self.data_flow.node_indices().map(|i| i.index()) + } + + fn is_operand(&self, sym: SymbolId) -> bool { + !matches!(self.data_flow[NodeIndex::new(sym)], Symbol::Operator(_)) + } + + fn traverse(&self, n: SymbolId, visit_map: &mut HashMap, v: &mut V) -> R + where + V: FormulaVisitor, + R: Clone, + { + if let Some(result) = visit_map.get(&n) { + return (*result).clone(); } - Node::Constant(c) => v.constant(n, BitVector(*c)), - Node::Input(name) => v.input(n, name.as_str()), - }; - visit_map.insert(n, result.clone()); + let result = match &self.data_flow[NodeIndex::new(n)] { + Symbol::Operator(op) => { + let mut operands = self + .data_flow + .neighbors_directed(NodeIndex::new(n), Direction::Incoming) + .detach(); + + if op.is_unary() { + let x = operands + .next(self.data_flow) + .expect("every unary operator must have 1 operand") + .1 + .index(); - result -} + let x = self.traverse(x, visit_map, v); -pub trait FormulaVisitor: Sized { - fn input(&mut self, idx: SymbolId, name: &str) -> T; - fn constant(&mut self, idx: SymbolId, v: BitVector) -> T; - fn unary(&mut self, idx: SymbolId, op: BVOperator, v: T) -> T; - fn binary(&mut self, idx: SymbolId, op: BVOperator, lhs: T, rhs: T) -> T; + v.unary(n, *op, x) + } else { + let lhs = operands + .next(self.data_flow) + .expect("every binary operator must have an lhs operand") + .1 + .index(); + + let rhs = operands + .next(self.data_flow) + .expect("every binary operator must have an rhs operand") + .1 + .index(); + + let lhs = self.traverse(lhs, visit_map, v); + let rhs = self.traverse(rhs, visit_map, v); + + v.binary(n, *op, lhs, rhs) + } + } + Symbol::Constant(c) => v.constant(n, *c), + Symbol::Input(name) => v.input(n, name.as_str()), + }; + + visit_map.insert(n, result.clone()); + + result + } } struct Printer {} -impl FormulaVisitor for Printer { +impl<'a> FormulaVisitor for Printer { fn input(&mut self, idx: SymbolId, name: &str) -> SymbolId { - debug!("x{} := {:?}", idx.index(), name); + debug!("x{} := {:?}", idx, name); idx } fn constant(&mut self, idx: SymbolId, v: BitVector) -> SymbolId { - debug!("x{} := {}", idx.index(), v.0); + debug!("x{} := {}", idx, v.0); idx } fn unary(&mut self, idx: SymbolId, op: BVOperator, v: SymbolId) -> SymbolId { - debug!("x{} := {}x{}", idx.index(), op, v.index()); + debug!("x{} := {}x{}", idx, op, v); idx } fn binary(&mut self, idx: SymbolId, op: BVOperator, lhs: SymbolId, rhs: SymbolId) -> SymbolId { - debug!( - "x{} := x{} {} x{}", - idx.index(), - lhs.index(), - op, - rhs.index() - ); + debug!("x{} := x{} {} x{}", idx, lhs, op, rhs); idx } } diff --git a/src/lib.rs b/src/lib.rs index bf94afc3..4d0f88bd 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,9 +1,79 @@ #[macro_use] pub mod util; -pub mod bug; pub mod disassemble; pub mod engine; pub mod path_exploration; pub mod solver; -pub mod symbolic_state; + +use engine::{Bug, Engine, EngineError, EngineOptions}; +use riscu::{load_object_file, Program}; +use std::path::Path; +use thiserror::Error; + +#[derive(Debug, Error)] +pub enum MonsterError { + #[error("I/O error")] + IoError(anyhow::Error), + + #[error("preprocessing failed with error")] + Preprocessing(anyhow::Error), + + #[error("execution stopped with error")] + Execution(EngineError), +} + +pub fn load_elf

(input: P) -> Result +where + P: AsRef, +{ + load_object_file(input).map_err(|e| { + MonsterError::IoError(anyhow::Error::new(e).context("Failed to load object file")) + }) +} + +pub fn execute(program: &Program) -> Result, MonsterError> { + let options = EngineOptions::default(); + let solver = solver::MonsterSolver::default(); + let strategy = path_exploration::ShortestPathStrategy::compute_for(program) + .map_err(MonsterError::Preprocessing)?; + + execute_with(program, &options, &strategy, &solver) +} + +pub fn execute_elf>(input: P) -> Result, MonsterError> { + let program = load_elf(input)?; + + execute(&program) +} + +pub fn execute_with( + program: &Program, + options: &EngineOptions, + strategy: &Strategy, + solver: &Solver, +) -> Result, MonsterError> +where + Strategy: path_exploration::ExplorationStrategy, + Solver: solver::Solver, +{ + let mut engine = Engine::new(&program, &options, strategy, solver); + + engine.run().map_err(MonsterError::Execution) +} + +pub fn execute_elf_with( + input: P, + options: &EngineOptions, + strategy: &Strategy, + solver: &Solver, +) -> Result, MonsterError> +where + P: AsRef, + Strategy: path_exploration::ExplorationStrategy, + Solver: solver::Solver, +{ + let program = load_elf(input)?; + + execute_with(&program, options, strategy, solver) +} diff --git a/src/main.rs b/src/main.rs index 0096b77f..8e19b356 100644 --- a/src/main.rs +++ b/src/main.rs @@ -7,8 +7,10 @@ use env_logger::{Env, TimestampPrecision}; use log::info; use monster::{ disassemble::disassemble, - engine, + engine::{self, EngineOptions}, + execute_elf_with, path_exploration::{ControlFlowGraph, ShortestPathStrategy}, + solver, }; use riscu::load_object_file; use std::{env, fmt::Display, fs::File, io::Write, path::Path}; @@ -57,28 +59,42 @@ fn main() -> Result<()> { .value_of_t::("memory") .expect("value is validated already"); - if let Some(bug) = engine::execute( - input, - match solver { - "monster" => engine::Backend::Monster, - "external" => engine::Backend::External, - - #[cfg(feature = "boolector-solver")] - "boolector" => engine::Backend::Boolector, - - #[cfg(feature = "z3-solver")] - "z3" => engine::Backend::Z3, - _ => unreachable!(), - }, - depth, - ByteSize::mb(megabytes), - ) + let options = EngineOptions { + max_exection_depth: depth, + memory_size: ByteSize::mb(megabytes), + }; + + let program = load_object_file(input)?; + + let strategy = ShortestPathStrategy::compute_for(&program)?; + + if let Some(bug) = match solver { + "monster" => execute_elf_with( + input, + &options, + &strategy, + &solver::MonsterSolver::default(), + ), + "external" => execute_elf_with( + input, + &options, + &strategy, + &solver::ExternalSolver::default(), + ), + #[cfg(feature = "boolector-solver")] + "boolector" => { + execute_elf_with(input, &options, &strategy, &solver::Boolector::default()) + } + #[cfg(feature = "z3-solver")] + "z3" => execute_elf_with(input, &options, &strategy, &solver::Z3::default()), + _ => unreachable!(), + } .with_context(|| format!("Execution of {} failed", input.display()))? { info!("bug found:\n{}", bug); } else { info!("no bug found in binary"); - } + }; Ok(()) } diff --git a/src/solver/boolector.rs b/src/solver/boolector.rs index 34e98f47..2490ba87 100644 --- a/src/solver/boolector.rs +++ b/src/solver/boolector.rs @@ -1,7 +1,6 @@ -use super::{Assignment, BitVector, Solver, SolverError}; -use crate::symbolic_state::{ - get_operands, BVOperator, Formula, - Node::{Constant, Input, Operator}, +use super::{ + Assignment, BVOperator, BitVector, Formula, Solver, SolverError, + Symbol::{Constant, Input, Operator}, SymbolId, }; use boolector::{ @@ -29,24 +28,20 @@ impl Solver for Boolector { "Boolector" } - fn solve_impl( - &self, - graph: &Formula, - root: SymbolId, - ) -> Result>, SolverError> { + fn solve_impl(&self, formula: &F) -> Result, SolverError> { let solver = Rc::new(Btor::new()); solver.set_opt(BtorOption::ModelGen(ModelGen::All)); solver.set_opt(BtorOption::Incremental(true)); solver.set_opt(BtorOption::OutputFileFormat(OutputFileFormat::SMTLIBv2)); let mut bvs = HashMap::new(); - let bv = traverse(graph, root, &solver, &mut bvs); + let bv = traverse(formula, formula.root(), &solver, &mut bvs); bv.slice(0, 0).assert(); match solver.sat() { SolverResult::Sat => { - let assignments = graph - .node_indices() + let assignments = formula + .symbol_ids() .filter_map(|i| { if let Some(bv) = bvs.get(&i) { Some(( @@ -71,55 +66,53 @@ impl Solver for Boolector { } } -fn traverse<'a>( - graph: &Formula, - node: SymbolId, +fn traverse<'a, F: Formula>( + formula: &F, + sym: SymbolId, solver: &'a Rc, bvs: &mut HashMap>>, ) -> BV> { let bv = - match &graph[node] { - Operator(op) => { - match get_operands(graph, node) { - (lhs, Some(rhs)) => match op { - BVOperator::Add => traverse(graph, lhs, solver, bvs) - .add(&traverse(graph, rhs, solver, bvs)), - BVOperator::Sub => traverse(graph, lhs, solver, bvs) - .sub(&traverse(graph, rhs, solver, bvs)), - BVOperator::Mul => traverse(graph, lhs, solver, bvs) - .mul(&traverse(graph, rhs, solver, bvs)), - BVOperator::Equals => traverse(graph, lhs, solver, bvs) - ._eq(&traverse(graph, rhs, solver, bvs)) - .uext(63), - BVOperator::BitwiseAnd => traverse(graph, lhs, solver, bvs) - .and(&traverse(graph, rhs, solver, bvs)), - BVOperator::Divu => traverse(graph, lhs, solver, bvs) - .udiv(&traverse(graph, rhs, solver, bvs)), - BVOperator::Remu => traverse(graph, lhs, solver, bvs) - .urem(&traverse(graph, rhs, solver, bvs)), - BVOperator::Sltu => traverse(graph, lhs, solver, bvs) - .ult(&traverse(graph, rhs, solver, bvs)) - .uext(63), - i => unreachable!("binary operator: {:?}", i), - }, - (lhs, None) => match op { - BVOperator::Not => traverse(graph, lhs, solver, bvs) - ._eq(&BV::from_u64(solver.clone(), 0, 64)) - .uext(63), - i => unreachable!("unary operator: {:?}", i), - }, - } - } + match &formula[sym] { + Operator(op) => match formula.operands(sym) { + (lhs, Some(rhs)) => match op { + BVOperator::Add => traverse(formula, lhs, solver, bvs) + .add(&traverse(formula, rhs, solver, bvs)), + BVOperator::Sub => traverse(formula, lhs, solver, bvs) + .sub(&traverse(formula, rhs, solver, bvs)), + BVOperator::Mul => traverse(formula, lhs, solver, bvs) + .mul(&traverse(formula, rhs, solver, bvs)), + BVOperator::Equals => traverse(formula, lhs, solver, bvs) + ._eq(&traverse(formula, rhs, solver, bvs)) + .uext(63), + BVOperator::BitwiseAnd => traverse(formula, lhs, solver, bvs) + .and(&traverse(formula, rhs, solver, bvs)), + BVOperator::Divu => traverse(formula, lhs, solver, bvs) + .udiv(&traverse(formula, rhs, solver, bvs)), + BVOperator::Remu => traverse(formula, lhs, solver, bvs) + .urem(&traverse(formula, rhs, solver, bvs)), + BVOperator::Sltu => traverse(formula, lhs, solver, bvs) + .ult(&traverse(formula, rhs, solver, bvs)) + .uext(63), + i => unreachable!("binary operator: {:?}", i), + }, + (lhs, None) => match op { + BVOperator::Not => traverse(formula, lhs, solver, bvs) + ._eq(&BV::from_u64(solver.clone(), 0, 64)) + .uext(63), + i => unreachable!("unary operator: {:?}", i), + }, + }, Input(name) => { - if let Some(value) = bvs.get(&node) { + if let Some(value) = bvs.get(&sym) { value.clone() } else { BV::new(solver.clone(), 64, Some(name)) } } - Constant(c) => BV::from_u64(solver.clone(), *c, 64), + Constant(c) => BV::from_u64(solver.clone(), (*c).0, 64), }; - bvs.insert(node, bv.clone()); + bvs.insert(sym, bv.clone()); bv } diff --git a/src/solver/external.rs b/src/solver/external.rs index 59f1858f..b95e121d 100644 --- a/src/solver/external.rs +++ b/src/solver/external.rs @@ -1,5 +1,6 @@ -use super::{Assignment, BitVector, Solver, SolverError}; -use crate::symbolic_state::{traverse, BVOperator, Formula, FormulaVisitor, SymbolId}; +use super::{ + Assignment, BVOperator, BitVector, Formula, FormulaVisitor, Solver, SolverError, SymbolId, +}; use std::{ collections::HashMap, fs::File, @@ -9,7 +10,7 @@ use std::{ }; pub struct ExternalSolver { - output: Arc>, + output: Arc>, } impl ExternalSolver { @@ -50,11 +51,7 @@ impl Solver for ExternalSolver { "External" } - fn solve_impl( - &self, - formula: &Formula, - root: SymbolId, - ) -> Result>, SolverError> { + fn solve_impl(&self, formula: &F) -> Result, SolverError> { { let mut output = self.output.lock().expect("no other thread should fail"); @@ -68,7 +65,7 @@ impl Solver for ExternalSolver { }; let mut visited = HashMap::>::new(); - traverse(formula, root, &mut visited, &mut printer)?; + formula.traverse(formula.root(), &mut visited, &mut printer)?; let mut output = self.output.lock().expect("no other thread should fail"); @@ -86,12 +83,7 @@ impl FormulaVisitor> for SmtPrinter { fn input(&mut self, idx: SymbolId, name: &str) -> Result { let mut o = self.output.lock().expect("no other thread should fail"); - writeln!( - o, - "(declare-fun x{} () (_ BitVec 64)); {:?}", - idx.index(), - name - )?; + writeln!(o, "(declare-fun x{} () (_ BitVec 64)); {:?}", idx, name)?; Ok(idx) } @@ -102,9 +94,7 @@ impl FormulaVisitor> for SmtPrinter { writeln!( o, "(declare-fun x{} () (_ BitVec 64))\n(assert (= x{} (_ bv{} 64)))", - idx.index(), - idx.index(), - v.0 + idx, idx, v.0 )?; Ok(idx) @@ -121,10 +111,10 @@ impl FormulaVisitor> for SmtPrinter { writeln!( o, "(declare-fun x{} () (_ BitVec 64))\n(assert (= x{} ({} x{})))", - idx.index(), - idx.index(), + idx, + idx, to_smt(op), - v?.index() + v? )?; Ok(idx) @@ -142,11 +132,11 @@ impl FormulaVisitor> for SmtPrinter { writeln!( o, "(declare-fun x{} () (_ BitVec 64))\n(assert (= x{} ({} x{} x{})))", - idx.index(), - idx.index(), + idx, + idx, to_smt(op), - lhs?.index(), - rhs?.index() + lhs?, + rhs? )?; Ok(idx) diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 9373f7e8..7e1f6875 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -16,33 +16,23 @@ pub use self::z3::*; pub use self::{bitvec::*, external::*, monster::*}; -use crate::symbolic_state::{Formula, SymbolId}; use log::debug; -use std::{collections::HashMap, convert::From, io}; +use std::marker::Sync; +use std::{collections::HashMap, convert::From, fmt, io, ops::Index}; use thiserror::Error; -pub type Assignment = HashMap; +pub type Assignment = HashMap; -pub trait Solver: Default { +pub trait Solver: Default + Sync { fn name() -> &'static str; - fn solve( - &self, - formula: &Formula, - root: SymbolId, - ) -> Result>, SolverError> { + fn solve(&self, formula: &F) -> Result, SolverError> { debug!("try to solve with {} solver", Self::name()); - time_debug!("finished solving formula", { - self.solve_impl(formula, root) - }) + time_debug!("finished solving formula", { self.solve_impl(formula) }) } - fn solve_impl( - &self, - formula: &Formula, - root: SymbolId, - ) -> Result>, SolverError>; + fn solve_impl(&self, formula: &F) -> Result, SolverError>; } #[derive(Debug, Error, Clone)] @@ -62,3 +52,103 @@ impl From for SolverError { SolverError::IoError(err.to_string()) } } + +#[derive(Clone, Debug, Copy, Eq, Hash, PartialEq)] +pub enum OperandSide { + Lhs, + Rhs, +} + +impl OperandSide { + #[allow(dead_code)] + pub fn other(&self) -> Self { + match self { + OperandSide::Lhs => OperandSide::Rhs, + OperandSide::Rhs => OperandSide::Lhs, + } + } +} + +#[derive(Debug, Copy, Clone, Hash, Eq, PartialEq)] +pub enum BVOperator { + Add, + Sub, + Mul, + Divu, + Sltu, + Remu, + Not, + Equals, + BitwiseAnd, +} + +impl BVOperator { + pub fn is_unary(&self) -> bool { + *self == BVOperator::Not + } + pub fn is_binary(&self) -> bool { + !self.is_unary() + } +} + +impl fmt::Display for BVOperator { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + write!( + f, + "{}", + match self { + BVOperator::Add => "+", + BVOperator::Sub => "-", + BVOperator::Mul => "*", + BVOperator::Divu => "/", + BVOperator::Not => "!", + BVOperator::Remu => "%", + BVOperator::Equals => "=", + BVOperator::BitwiseAnd => "&", + BVOperator::Sltu => "<", + } + ) + } +} + +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +pub enum Symbol { + Constant(BitVector), + Input(String), + Operator(BVOperator), +} + +pub type SymbolId = usize; + +pub trait Formula: Index { + type DependencyIter: Iterator; + type SymbolIdsIter: Iterator; + + fn root(&self) -> SymbolId; + + fn operands(&self, sym: SymbolId) -> (SymbolId, Option); + + fn operand(&self, sym: SymbolId) -> SymbolId; + + fn dependencies(&self, sym: SymbolId) -> Self::DependencyIter; + //where + //Iter: Iterator; + + fn symbol_ids(&self) -> Self::SymbolIdsIter; + //where + //Iter: Iterator; + + fn is_operand(&self, sym: SymbolId) -> bool; + + fn traverse(&self, n: SymbolId, visit_map: &mut HashMap, v: &mut V) -> R + where + V: FormulaVisitor, + R: Clone; +} + +pub trait FormulaVisitor: Sized { + fn input(&mut self, idx: SymbolId, name: &str) -> T; + fn constant(&mut self, idx: SymbolId, v: BitVector) -> T; + fn unary(&mut self, idx: SymbolId, op: BVOperator, v: T) -> T; + fn binary(&mut self, idx: SymbolId, op: BVOperator, lhs: T, rhs: T) -> T; +} diff --git a/src/solver/monster.rs b/src/solver/monster.rs index 52116085..50d9badb 100644 --- a/src/solver/monster.rs +++ b/src/solver/monster.rs @@ -2,25 +2,27 @@ #![allow(clippy::if_same_then_else)] #![allow(clippy::neg_cmp_op_on_partial_ord)] -use super::{Assignment, BitVector, Solver, SolverError}; -use crate::symbolic_state::{get_operands, BVOperator, Formula, Node, OperandSide, SymbolId}; +use super::{ + Assignment, BVOperator, BitVector, Formula, OperandSide, Solver, SolverError, Symbol, SymbolId, +}; use divisors::get_divisors; use log::{log_enabled, trace, Level}; -use petgraph::{visit::EdgeRef, Direction}; use rand::{distributions::Uniform, random, seq::SliceRandom, thread_rng, Rng}; use std::time::{Duration, Instant}; -pub struct MonsterSolver {} +pub struct MonsterSolver { + timeout: Duration, +} impl Default for MonsterSolver { fn default() -> Self { - Self::new() + Self::new(Duration::new(3, 0)) } } impl MonsterSolver { - pub fn new() -> Self { - Self {} + pub fn new(timeout: Duration) -> Self { + Self { timeout } } } @@ -29,16 +31,10 @@ impl Solver for MonsterSolver { "Monster" } - fn solve_impl( - &self, - formula: &Formula, - root: SymbolId, - ) -> Result>, SolverError> { + fn solve_impl(&self, formula: &F) -> Result, SolverError> { let ab = initialize_ab(formula); - let timeout_time = Duration::new(5, 0); - - sat(formula, root, ab, timeout_time) + sat(formula, ab, self.timeout) } } @@ -97,38 +93,41 @@ fn is_invertable(op: BVOperator, s: BitVector, t: BitVector, d: OperandSide) -> } } -fn is_leaf(formula: &Formula, idx: SymbolId) -> bool { - let incoming = formula.edges_directed(idx, Direction::Incoming).count(); - - incoming == 0 -} - // initialize bit vectors with a consistent intial assignment to the formula // inputs are initialized with random values -fn initialize_ab(formula: &Formula) -> Vec { +fn initialize_ab(formula: &F) -> Vec { // Initialize values for all input/const nodes - let mut ab = formula - .node_indices() - .map(|i| match formula[i] { - Node::Constant(c) => BitVector(c), + let max_id = formula + .symbol_ids() + .max() + .expect("formula should not be empty"); + + let mut ab = Vec::with_capacity(std::mem::size_of::() * (max_id + 1)); + unsafe { + ab.set_len(max_id + 1); + } + + formula.symbol_ids().for_each(|i| { + ab[i] = match formula[i] { + Symbol::Constant(c) => c, _ => BitVector(random::()), - }) - .collect::>(); + }; + }); if log_enabled!(Level::Trace) { formula - .node_indices() - .filter(|i| matches!(formula[*i], Node::Input(_))) + .symbol_ids() + .filter(|i| matches!(formula[*i], Symbol::Input(_))) .for_each(|i| { - trace!("initialize: x{} <- {:#x}", i.index(), ab[i.index()].0); + trace!("initialize: x{} <- {:#x}", i, ab[i].0); }); } // Propagate all values down when all input/const nodes are initialized - formula.node_indices().for_each(|i| match formula[i] { - Node::Input(_) | Node::Constant(_) => { + formula.symbol_ids().for_each(|i| match formula[i] { + Symbol::Input(_) | Symbol::Constant(_) => { formula - .neighbors_directed(i, Direction::Outgoing) + .dependencies(i) .for_each(|n| propagate_assignment(formula, &mut ab, n)); } _ => {} @@ -140,15 +139,15 @@ fn initialize_ab(formula: &Formula) -> Vec { // selects a child node to propagate downwards // always selects an "essential" input if there is one // otherwise selects an input undeterministically -fn select( - f: &Formula, +fn select( + f: &F, idx: SymbolId, t: BitVector, ab: &[BitVector], ) -> (SymbolId, SymbolId, OperandSide) { - if let (lhs, Some(rhs)) = get_operands(f, idx) { - fn is_constant(f: &Formula, n: SymbolId) -> bool { - matches!(f[n], Node::Constant(_)) + if let (lhs, Some(rhs)) = f.operands(idx) { + fn is_constant(f: &F, n: SymbolId) -> bool { + matches!(f[n], Symbol::Constant(_)) } #[allow(clippy::if_same_then_else)] @@ -398,18 +397,18 @@ const CHOOSE_INVERSE: f64 = 0.90; // computes an inverse/consistent target value #[allow(clippy::too_many_arguments)] -fn value( - f: &Formula, +fn value( + f: &F, n: SymbolId, ns: SymbolId, side: OperandSide, t: BitVector, ab: &[BitVector], ) -> BitVector { - let s = ab[ns.index()]; + let s = ab[ns]; match &f[n] { - Node::Operator(op) => { + Symbol::Operator(op) => { let consistent = compute_consistent_value(*op, t, side); if is_invertable(*op, s, t, side) { @@ -430,95 +429,88 @@ fn value( } } -fn is_essential( - formula: &Formula, +fn is_essential( + formula: &F, this: SymbolId, on_side: OperandSide, other: SymbolId, t: BitVector, ab: &[BitVector], ) -> bool { - let ab_nx = ab[this.index()]; + let ab_nx = ab[this]; match &formula[other] { - Node::Operator(op) => !is_invertable(*op, ab_nx, t, on_side.other()), + Symbol::Operator(op) => !is_invertable(*op, ab_nx, t, on_side.other()), // TODO: not mentioned in paper => improvised. is that really true? - Node::Constant(_) | Node::Input(_) => false, + Symbol::Constant(_) | Symbol::Input(_) => false, } } -fn get_operand(f: &Formula, n: SymbolId) -> SymbolId { - f.edges_directed(n, Direction::Incoming) - .next() - .expect("every unary operator must have an operand") - .source() -} - -fn update_assignment(f: &Formula, ab: &mut Vec, n: SymbolId, v: BitVector) { - ab[n.index()] = v; +fn update_assignment(f: &F, ab: &mut Vec, n: SymbolId, v: BitVector) { + ab[n] = v; assert!( - matches!(f[n], Node::Input(_)), + matches!(f[n], Symbol::Input(_)), "only inputs can be assigned" ); - trace!("update: x{} <- {:#x}", n.index(), v.0); + trace!("update: x{} <- {:#x}", n, v.0); - f.neighbors_directed(n, Direction::Outgoing) + f.dependencies(n) .for_each(|n| propagate_assignment(f, ab, n)); } -fn propagate_assignment(f: &Formula, ab: &mut Vec, n: SymbolId) { - fn update_binary(f: &Formula, ab: &mut Vec, n: SymbolId, s: &str, op: Op) +fn propagate_assignment(f: &F, ab: &mut Vec, n: SymbolId) { + fn update_binary(f: &F, ab: &mut Vec, n: SymbolId, s: &str, op: Op) where Op: FnOnce(BitVector, BitVector) -> BitVector, { - if let (lhs, Some(rhs)) = get_operands(f, n) { - let result = op(ab[lhs.index()], ab[rhs.index()]); + if let (lhs, Some(rhs)) = f.operands(n) { + let result = op(ab[lhs], ab[rhs]); trace!( "propagate: x{} := x{}({:#x}) {} x{}({:#x}) |- x{} <- {:#x}", - n.index(), - lhs.index(), - ab[lhs.index()].0, + n, + lhs, + ab[lhs].0, s, - rhs.index(), - ab[rhs.index()].0, - n.index(), + rhs, + ab[rhs].0, + n, result.0 ); - ab[n.index()] = result; + ab[n] = result; } else { panic!("can not update binary operator with 1 operand") } } - fn update_unary(f: &Formula, ab: &mut Vec, n: SymbolId, s: &str, op: Op) + fn update_unary(f: &F, ab: &mut Vec, n: SymbolId, s: &str, op: Op) where Op: FnOnce(BitVector) -> BitVector, { - if let (p, None) = get_operands(f, n) { - let result = op(ab[p.index()]); + if let (p, None) = f.operands(n) { + let result = op(ab[p]); trace!( "propagate: x{} := {}x{}({:#x}) |- x{} <- {:#x}", - n.index(), + n, s, - p.index(), - ab[p.index()].0, - n.index(), + p, + ab[p].0, + n, result.0 ); - ab[n.index()] = result; + ab[n] = result; } else { panic!("can not update unary operator with more than one operand") } } match &f[n] { - Node::Operator(op) => { + Symbol::Operator(op) => { match op { BVOperator::Add => update_binary(f, ab, n, "+", |l, r| l + r), BVOperator::Sub => update_binary(f, ab, n, "-", |l, r| l - r), @@ -548,51 +540,53 @@ fn propagate_assignment(f: &Formula, ab: &mut Vec, n: SymbolId) { } }), } - f.neighbors_directed(n, Direction::Outgoing) + f.dependencies(n) + //f.neighbors_directed(n, Direction::Outgoing) .for_each(|n| propagate_assignment(f, ab, n)); } _ => unreachable!(), } } -// can only handle one Equals constrain with constant -fn sat( - formula: &Formula, - root: SymbolId, +// can only handle one Equals constraint with constant +fn sat( + formula: &F, mut ab: Vec, timeout_time: Duration, -) -> Result>, SolverError> { +) -> Result, SolverError> { let mut iterations = 0; let start_time = Instant::now(); - while ab[root.index()] != BitVector(1) { + let root = formula.root(); + + while ab[root] != BitVector(1) { let mut n = root; let mut t = BitVector(1); iterations += 1; - trace!("search {}: x{} <- 0x1", iterations, root.index()); + trace!("search {}: x{} <- 0x1", iterations, root); - while !is_leaf(formula, n) { + while !formula.is_operand(n) { if start_time.elapsed() > timeout_time { return Err(SolverError::Timeout); } let (v, nx) = match formula[n] { - Node::Operator(op) => { + Symbol::Operator(op) => { if op.is_unary() { - let nx = get_operand(formula, n); + let nx = formula.operand(n); let v = compute_inverse_value_for_unary_op(op, t); trace!( "search {}: x{}({:#x}) = {}x{}({:#x}) |- x{} <- {:#x}", iterations, - n.index(), + n, t.0, op, - nx.index(), - ab[nx.index()].0, - nx.index(), + nx, + ab[nx].0, + nx, v.0 ); @@ -612,14 +606,14 @@ fn sat( trace!( "search {}: x{}({:#x}) := x{}({:#x}) {} x{}({:#x}) |- x{} <- {:#x}", iterations, - n.index(), + n, t.0, - lhs.index(), - ab[lhs.index()].0, + lhs, + ab[lhs].0, op, - rhs.index(), - ab[rhs.index()].0, - nx.index(), + rhs, + ab[rhs].0, + nx, v.0 ); } @@ -637,7 +631,7 @@ fn sat( update_assignment(formula, &mut ab, n, t); } - let assignment: Assignment<_> = formula.node_indices().map(|i| (i, ab[i.index()])).collect(); + let assignment: Assignment = formula.symbol_ids().map(|i| (i, ab[i])).collect(); Ok(Some(assignment)) } @@ -645,53 +639,55 @@ fn sat( #[cfg(test)] mod tests { use super::*; - //use crate::engine::SyscallId::Openat; + use crate::engine::symbolic_state::{DataFlowGraph, FormulaView, SymbolicValue}; + use crate::solver::*; - fn create_formula_with_input() -> (Formula, SymbolId) { - let mut formula = Formula::new(); + fn create_data_flow_with_input() -> (DataFlowGraph, SymbolicValue) { + let mut formula = DataFlowGraph::new(); - let input = Node::Input(String::from("x0")); + let input = Symbol::Input(String::from("x0")); let input_idx = formula.add_node(input); (formula, input_idx) } - fn add_equals_constrain( - formula: &mut Formula, - to: SymbolId, + fn add_equals_constraint( + data_flow: &mut DataFlowGraph, + to: SymbolicValue, on: OperandSide, constant: u64, - ) -> SymbolId { - let constrain = Node::Operator(BVOperator::Equals); - let constrain_idx = formula.add_node(constrain); + ) -> SymbolicValue { + let constrain = Symbol::Operator(BVOperator::Equals); + let constrain_idx = data_flow.add_node(constrain); - let constrain_c = Node::Constant(constant); - let constrain_c_idx = formula.add_node(constrain_c); + let constrain_c = Symbol::Constant(BitVector(constant)); + let constrain_c_idx = data_flow.add_node(constrain_c); - formula.add_edge(to, constrain_idx, on); - formula.add_edge(constrain_c_idx, constrain_idx, on.other()); + data_flow.add_edge(to, constrain_idx, on); + data_flow.add_edge(constrain_c_idx, constrain_idx, on.other()); constrain_idx } #[test] - fn solve_trivial_equals_constrain() { - let (mut formula, input_idx) = create_formula_with_input(); + fn solve_trivial_equals_constraint() { + let (mut data_flow, input_idx) = create_data_flow_with_input(); - let root = add_equals_constrain(&mut formula, input_idx, OperandSide::Lhs, 10); + let root = add_equals_constraint(&mut data_flow, input_idx, OperandSide::Lhs, 10); let solver = MonsterSolver::default(); - let result = solver.solve(&formula, root); + let formula = FormulaView::new(&data_flow, root); + let result = solver.solve(&formula); assert!(result.is_ok(), "solver did not time out"); let unwrapped_result = result.unwrap(); assert!( unwrapped_result.is_some(), - "has result for trivial equals constrain" + "has result for trivial equals constraint" ); assert_eq!( - *unwrapped_result.unwrap().get(&input_idx).unwrap(), + *unwrapped_result.unwrap().get(&input_idx.index()).unwrap(), BitVector(10), "solver result of trivial equal constrain has right value" ); @@ -699,28 +695,29 @@ mod tests { #[test] fn solve_bvadd() { - let (mut formula, input_idx) = create_formula_with_input(); + let (mut data_flow, input_idx) = create_data_flow_with_input(); - let constant = Node::Constant(3); - let constant_idx = formula.add_node(constant); + let constant = Symbol::Constant(BitVector(3)); + let constant_idx = data_flow.add_node(constant); - let instr = Node::Operator(BVOperator::Add); - let instr_idx = formula.add_node(instr); + let instr = Symbol::Operator(BVOperator::Add); + let instr_idx = data_flow.add_node(instr); - formula.add_edge(input_idx, instr_idx, OperandSide::Lhs); - formula.add_edge(constant_idx, instr_idx, OperandSide::Rhs); + data_flow.add_edge(input_idx, instr_idx, OperandSide::Lhs); + data_flow.add_edge(constant_idx, instr_idx, OperandSide::Rhs); - let root = add_equals_constrain(&mut formula, instr_idx, OperandSide::Lhs, 10); + let root = add_equals_constraint(&mut data_flow, instr_idx, OperandSide::Lhs, 10); let solver = MonsterSolver::default(); - let result = solver.solve(&formula, root); + let formula = FormulaView::new(&data_flow, root); + let result = solver.solve(&formula); assert!(result.is_ok(), "solver did not time out"); let unwrapped_result = result.unwrap(); assert!(unwrapped_result.is_some(), "has result for trivial add op"); assert_eq!( - *unwrapped_result.unwrap().get(&input_idx).unwrap(), + *unwrapped_result.unwrap().get(&input_idx.index()).unwrap(), BitVector(7), "solver result of trivial add op has right value" ); diff --git a/src/solver/z3.rs b/src/solver/z3.rs index 80e3e269..e296d03e 100644 --- a/src/solver/z3.rs +++ b/src/solver/z3.rs @@ -1,7 +1,6 @@ -use super::{Assignment, BitVector, Solver, SolverError}; -use crate::symbolic_state::{ - get_operands, BVOperator, Formula, - Node::{Constant, Input, Operator}, +use super::{ + Assignment, BVOperator, BitVector, Formula, Solver, SolverError, + Symbol::{Constant, Input, Operator}, SymbolId, }; use std::collections::HashMap; @@ -29,17 +28,13 @@ impl Solver for Z3 { "Z3" } - fn solve_impl( - &self, - graph: &Formula, - root: SymbolId, - ) -> Result>, SolverError> { + fn solve_impl(&self, formula: &F) -> Result, SolverError> { let config = Config::default(); let ctx = Context::new(&config); - let mut translator = Z3Translator::new(graph, &ctx); + let mut translator = Z3Translator::new(formula, &ctx); - let (root_node, translation) = translator.translate(root); + let (root_node, translation) = translator.translate(formula.root()); let solver = Z3Solver::new(&ctx); @@ -52,8 +47,8 @@ impl Solver for Z3 { .expect("has an result after calling check()"); Ok(Some( - graph - .node_indices() + formula + .symbol_ids() .filter_map(|i| match bv_for_node_idx(i, translation, &model) { Some(bv) => Some((i, bv)), None => None, @@ -117,18 +112,18 @@ macro_rules! traverse_binary { }}; } -struct Z3Translator<'a, 'ctx> { - graph: &'a Formula, +struct Z3Translator<'a, 'ctx, F: Formula> { + formula: &'a F, ctx: &'ctx Context, bvs: HashMap>, zero: Dynamic<'ctx>, one: Dynamic<'ctx>, } -impl<'a, 'ctx> Z3Translator<'a, 'ctx> { - pub fn new(graph: &'a Formula, into: &'ctx Context) -> Self { +impl<'a, 'ctx, F: Formula> Z3Translator<'a, 'ctx, F> { + pub fn new(formula: &'a F, into: &'ctx Context) -> Self { Self { - graph, + formula, ctx: into, bvs: HashMap::new(), zero: Dynamic::from(BV::from_u64(into, 0, 64)), @@ -144,9 +139,9 @@ impl<'a, 'ctx> Z3Translator<'a, 'ctx> { (root_node._eq(&self.one), &self.bvs) } - fn traverse(&mut self, node: SymbolId) -> Dynamic<'ctx> { - let ast_node = match &self.graph[node] { - Operator(op) => match get_operands(self.graph, node) { + fn traverse(&mut self, sym: SymbolId) -> Dynamic<'ctx> { + let ast_node = match &self.formula[sym] { + Operator(op) => match self.formula.operands(sym) { (lhs, Some(rhs)) => match op { BVOperator::Add => traverse_binary!(self, lhs, bvadd, rhs), BVOperator::Sub => traverse_binary!(self, lhs, bvsub, rhs), @@ -173,16 +168,16 @@ impl<'a, 'ctx> Z3Translator<'a, 'ctx> { }, }, Input(name) => { - if let Some(value) = self.bvs.get(&node) { + if let Some(value) = self.bvs.get(&sym) { value.clone() } else { Dynamic::from(BV::new_const(self.ctx, name.clone(), 64)) } } - Constant(cst) => Dynamic::from(BV::from_u64(self.ctx, *cst, 64)), + Constant(cst) => Dynamic::from(BV::from_u64(self.ctx, (*cst).0, 64)), }; - self.bvs.insert(node, ast_node.clone()); + self.bvs.insert(sym, ast_node.clone()); ast_node } diff --git a/tests/common.rs b/tests/common.rs index 6471fcb0..08075f6b 100644 --- a/tests/common.rs +++ b/tests/common.rs @@ -2,7 +2,7 @@ use log::info; use rayon::{iter::ParallelBridge, prelude::*}; use std::{ env, - fs::{canonicalize, read_dir}, + fs::read_dir, path::{Path, PathBuf}, process::Command, sync::{Arc, Once}, @@ -29,11 +29,9 @@ pub fn compile

( where P: AsRef, { - let src = canonicalize(source_file.as_ref()).unwrap(); - Command::new(selfie_path.as_ref()) .arg("-c") - .arg(src) + .arg(source_file.as_ref()) .arg("-o") .arg(destination_file.as_ref()) .output() @@ -159,7 +157,9 @@ pub fn compile_riscu( ) -> impl ParallelIterator { let selfie_path = ensure_selfie_installed(); - read_dir("examples") + let examples_path = env::current_dir().unwrap().join("examples"); + + read_dir(examples_path) .unwrap() .par_bridge() .map(|dir_entry| dir_entry.unwrap().path()) diff --git a/tests/engine.rs b/tests/engine.rs index 7ea9db2d..a7ee1d62 100644 --- a/tests/engine.rs +++ b/tests/engine.rs @@ -3,9 +3,19 @@ mod common; use bytesize::ByteSize; use common::{compile_riscu, init, with_temp_dir}; use log::trace; -use monster::{self, bug::Bug, engine::*}; +use monster::{ + self, + engine::{Bug, EngineOptions}, + execute_with, load_elf, + path_exploration::ShortestPathStrategy, + solver::{MonsterSolver, Solver}, + MonsterError, +}; use rayon::prelude::*; -use std::path::PathBuf; +use std::{ + path::{Path, PathBuf}, + time::Duration, +}; const TEST_FILES: [&str; 14] = [ "arithmetic.c", @@ -26,22 +36,31 @@ const TEST_FILES: [&str; 14] = [ //"three-level-nested-loop-1-35", ]; -// TODO: Fix this test case #[test] fn execute_riscu_with_monster_solver() { - execute_riscu_examples(&TEST_FILES, Backend::Monster); + // need a big timeout because of the slow Github runners + let solver = MonsterSolver::new(Duration::new(5, 0)); + execute_riscu_examples(&TEST_FILES, &solver); } #[test] #[cfg(feature = "boolector-solver")] fn execute_riscu_with_boolector_solver() { - execute_riscu_examples(&TEST_FILES, Backend::Boolector); + use monster::solver::Boolector; + + let solver = Boolector::default(); + + execute_riscu_examples(&TEST_FILES, &solver); } #[test] #[cfg(feature = "z3-solver")] fn execute_riscu_with_z3_solver() { - execute_riscu_examples(&TEST_FILES, Backend::Z3); + use monster::solver::Z3; + + let solver = Z3::default(); + + execute_riscu_examples(&TEST_FILES, &solver); } #[test] @@ -51,7 +70,12 @@ fn execute_with_different_memory_sizes() { with_temp_dir(|dir| { compile_riscu(dir, Some(&["recursive-fibonacci-1-35.c"])).for_each(|(source, object)| { [1, 64, 512, 1024].iter().for_each(move |size| { - let result = execute(&object, Backend::Monster, 200, ByteSize::mb(*size)); + let options = EngineOptions { + max_exection_depth: 200, + memory_size: ByteSize::mb(*size), + }; + + let result = execute_default_with(&object, &options); assert!( result.is_ok(), @@ -71,15 +95,41 @@ fn execute_engine_for_endless_loops() { with_temp_dir(|dir| { compile_riscu(dir, Some(&["endless-loop.c"])).for_each(|(_, object)| { + let options = EngineOptions { + max_exection_depth: 5, + ..Default::default() + }; + assert!( - execute(object, Backend::Monster, 5, ByteSize::mb(1)).is_err(), + execute_default_with(object, &options).is_err(), "has to error with depth error" ); }); }); } -fn execute_riscu_examples(names: &'static [&str], solver: Backend) { +fn execute_default_with>( + object: P, + options: &EngineOptions, +) -> Result, MonsterError> { + // need a big timeout because of the slow Github runners + let solver = MonsterSolver::new(Duration::new(5, 0)); + + execute_default_with_solver(object, options, &solver) +} + +fn execute_default_with_solver, S: Solver>( + object: P, + options: &EngineOptions, + solver: &S, +) -> Result, MonsterError> { + let program = load_elf(object).unwrap(); + let strategy = ShortestPathStrategy::compute_for(&program).unwrap(); + + execute_with(&program, options, &strategy, solver) +} + +fn execute_riscu_examples(names: &'static [&str], solver: &S) { init(); with_temp_dir(|dir| { @@ -88,16 +138,19 @@ fn execute_riscu_examples(names: &'static [&str], solver: Backend) { }); } -fn execute_riscu(source: PathBuf, object: PathBuf, solver: Backend) { +fn execute_riscu(source: PathBuf, object: PathBuf, solver: &S) { let file_name = source.file_name().unwrap().to_str().unwrap(); - let depth = match file_name { - "two-level-nested-loop-1-35.c" => 200, - "recursive-fibonacci-1-10.c" => 300, - _ => 1000, + let options = EngineOptions { + max_exection_depth: match file_name { + "two-level-nested-loop-1-35.c" => 200, + "recursive-fibonacci-1-10.c" => 300, + _ => 1000, + }, + ..Default::default() }; - let result = execute(object, solver, depth, ByteSize::mb(1)); + let result = execute_default_with_solver(object, &options, solver); trace!("execution finished: {:?}", result);