From 9d5e6512b482de3f52ffd19b96a0567a0d375167 Mon Sep 17 00:00:00 2001 From: finga Date: Thu, 10 Sep 2020 10:02:51 +0200 Subject: [PATCH] Add smt generation and solving Use the patched `boolector-sys` crate for now. This closes #16. --- Cargo.lock | 67 +++++++++++++++++++++++++------- Cargo.toml | 1 + src/cli.rs | 1 + src/formula_graph.rs | 92 ++++++++++++++++++++++---------------------- src/main.rs | 63 ++++++++++++++++++++++++++++++ src/smt.rs | 78 +++++++++++++++++++++++++++++++++++++ 6 files changed, 243 insertions(+), 59 deletions(-) create mode 100644 src/smt.rs diff --git a/Cargo.lock b/Cargo.lock index 0ab223b2..5d5e4708 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -23,6 +23,34 @@ version = "1.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cf1de2fe8c75bc145a2f577add951f8134889b4795d47466a54a5c846d691693" +[[package]] +name = "boolector" +version = "0.4.1" +source = "git+https://github.com/finga/boolector-rs?branch=boolector-src#9d384944a795edf6baea2dd7d0bddf35cdae79ca" +dependencies = [ + "boolector-sys", + "libc", +] + +[[package]] +name = "boolector-src" +version = "0.1.0-alpha+3.2.1" +source = "git+https://github.com/finga/boolector-src-rs#da4443af58cf69e52c8e9a22062e1be46bf44e6a" +dependencies = [ + "cc", + "cmake", +] + +[[package]] +name = "boolector-sys" +version = "0.5.0" +source = "git+https://github.com/finga/boolector-sys?branch=boolector-src#20e7265f398c52af3655428bc603f5e76b73d2c1" +dependencies = [ + "boolector-src", + "cc", + "libc", +] + [[package]] name = "byteorder" version = "1.3.4" @@ -35,6 +63,12 @@ version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7b02b629252fe8ef6460461409564e2c21d0c8e77e0944f3d189ff06c4e932ad" +[[package]] +name = "cc" +version = "1.0.60" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ef611cc68ff783f18535d77ddd080185275713d852c4f5cbb6122c462a7a825c" + [[package]] name = "cfg-if" version = "0.1.10" @@ -82,6 +116,15 @@ dependencies = [ "bitflags", ] +[[package]] +name = "cmake" +version = "0.1.44" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0e56268c17a6248366d66d4a47a3381369d068cce8409bb1716ed77ea32163bb" +dependencies = [ + "cc", +] + [[package]] name = "fixedbitset" version = "0.2.0" @@ -112,12 +155,9 @@ dependencies = [ [[package]] name = "hashbrown" -version = "0.8.2" +version = "0.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e91b62f79061a0bc2e046024cb7ba44b08419ed238ecbd9adbd787434b9e8c25" -dependencies = [ - "autocfg", -] +checksum = "00d63df3d41950fb462ed38308eea019113ad1508da725bbedcd0fa5a85ef5f7" [[package]] name = "heck" @@ -139,9 +179,9 @@ dependencies = [ [[package]] name = "indexmap" -version = "1.5.1" +version = "1.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "86b45e59b16c76b11bf9738fd5d38879d3bd28ad292d7b313608becb17ae2df9" +checksum = "55e2e4c765aa53a0424761bf9f41aa7a6ac1efa87238f59560640e27fca028f2" dependencies = [ "autocfg", "hashbrown", @@ -155,9 +195,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.76" +version = "0.2.77" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "755456fae044e6fa1ebbbd1b3e902ae19e73097ed4ed87bb79934a867c007bc3" +checksum = "f2f96b10ec2560088a8e76961b00d47107b3a625fecb76dedb29ee7ccbf98235" [[package]] name = "lock_api" @@ -181,6 +221,7 @@ dependencies = [ name = "monster" version = "0.1.0" dependencies = [ + "boolector", "byteorder", "cargo-husky", "clap", @@ -271,9 +312,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.19" +version = "1.0.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "04f5f085b5d71e2188cb8271e5da0161ad52c3f227a661a3c135fdf28e258b12" +checksum = "36e28516df94f3dd551a587da5357459d9b36d945a7c37c3557928c1c2ff2a2c" dependencies = [ "unicode-xid", ] @@ -401,9 +442,9 @@ checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623" [[package]] name = "syn" -version = "1.0.39" +version = "1.0.41" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "891d8d6567fe7c7f8835a3a98af4208f3846fba258c1bc3c31d6e506239f11f9" +checksum = "6690e3e9f692504b941dc6c3b188fd28df054f7fb8469ab40680df52fdcc842b" dependencies = [ "proc-macro2", "quote", diff --git a/Cargo.toml b/Cargo.toml index e2fccb65..e8fec703 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -12,6 +12,7 @@ clap = "3.0.0-beta.1" riscv-decode = { git = "https://github.com/cksystemsgroup/riscv-decode" } petgraph = "0.5.1" rand = "0.7.3" +boolector = { version = "0.4", git = "https://github.com/finga/boolector-rs", branch = "boolector-src", features = ["vendored"] } [dev-dependencies] serial_test = "0.4.0" diff --git a/src/cli.rs b/src/cli.rs index affafeed..e47606e8 100644 --- a/src/cli.rs +++ b/src/cli.rs @@ -75,6 +75,7 @@ pub fn args() -> App<'static> { .default_value("dot"), ), ) + .subcommand(App::new("smt")) .setting(AppSettings::SubcommandRequiredElseHelp) .global_setting(AppSettings::GlobalVersion) } diff --git a/src/formula_graph.rs b/src/formula_graph.rs index 2abb2f78..e35f1624 100644 --- a/src/formula_graph.rs +++ b/src/formula_graph.rs @@ -1,8 +1,10 @@ +use crate::cfg::ControlFlowGraph; use crate::elf::ElfMetadata; use crate::iterator::ForEachUntilSome; use byteorder::{ByteOrder, LittleEndian}; use core::fmt; pub use petgraph::graph::NodeIndex; +use petgraph::visit::EdgeRef; use petgraph::Graph; use riscv_decode::types::*; use riscv_decode::Instruction; @@ -126,7 +128,7 @@ impl fmt::Debug for Input { } #[allow(dead_code)] -#[derive(Clone, Eq, Hash, PartialEq)] +#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)] pub enum BooleanFunction { NotEqual, Equals, @@ -604,7 +606,7 @@ fn sign_extend_itype_stype(imm: u32) -> u64 { } #[allow(dead_code)] -fn build_dataflow_graph( +pub fn build_dataflow_graph( path: &[Instruction], data_segment: &[u8], elf_metadata: ElfMetadata, @@ -614,15 +616,55 @@ fn build_dataflow_graph( .generate_graph() } +// Returns a path of RISC-U instructions and branch decisions (if true or false branch has been taken) +// for a path with 1 BEQ instruction, the vector of branch decisions has the length of 1 +pub fn extract_candidate_path(graph: &ControlFlowGraph) -> (Vec, Vec) { + fn next(graph: &ControlFlowGraph, idx: NodeIndex) -> Option<(NodeIndex, Option)> { + let edges = graph.edges(idx); + + if let Some(edge) = edges.last() { + let target = edge.target(); + + match graph[idx] { + Instruction::Beq(_) => { + let next_idx = edge.target().index(); + + if next_idx == idx.index() + 1 { + Some((target, Some(false))) + } else { + Some((target, Some(true))) + } + } + _ => Some((target, None)), + } + } else { + None + } + } + let mut path = vec![]; + let mut branch_decisions = vec![]; + let mut idx = graph.node_indices().next().unwrap(); + path.push(idx); + while let Some(n) = next(graph, idx) { + path.push(n.0); + idx = n.0; + + if let Some(branch_decision) = n.1 { + branch_decisions.push(branch_decision); + } + } + let instruction_path = path.iter().map(|idx| graph[*idx]).collect(); + + (instruction_path, branch_decisions) +} + // TODO: need to load data segment => then write test #[cfg(test)] mod tests { use super::*; use crate::cfg; - use crate::cfg::ControlFlowGraph; use crate::dead_code_elimination::eliminate_dead_code; use petgraph::dot::Dot; - use petgraph::visit::EdgeRef; use serial_test::serial; use std::env::current_dir; use std::fs::File; @@ -630,48 +672,6 @@ mod tests { use std::path::Path; use std::process::Command; - // Returns a path of RISC-U instructions and branch decisions (if true or false branch has been taken) - // for a path with 1 BEQ instruction, the vector of branch decisions has the length of 1 - pub fn extract_candidate_path(graph: &ControlFlowGraph) -> (Vec, Vec) { - fn next(graph: &ControlFlowGraph, idx: NodeIndex) -> Option<(NodeIndex, Option)> { - let edges = graph.edges(idx); - - if let Some(edge) = edges.last() { - let target = edge.target(); - - match graph[idx] { - Instruction::Beq(_) => { - let next_idx = edge.target().index(); - - if next_idx == idx.index() + 1 { - Some((target, Some(false))) - } else { - Some((target, Some(true))) - } - } - _ => Some((target, None)), - } - } else { - None - } - } - let mut path = vec![]; - let mut branch_decisions = vec![]; - let mut idx = graph.node_indices().next().unwrap(); - path.push(idx); - while let Some(n) = next(graph, idx) { - path.push(n.0); - idx = n.0; - - if let Some(branch_decision) = n.1 { - branch_decisions.push(branch_decision); - } - } - let instruction_path = path.iter().map(|idx| graph[*idx]).collect(); - - (instruction_path, branch_decisions) - } - // TODO: write a unit test without dependency on selfie and external files #[test] #[serial] diff --git a/src/main.rs b/src/main.rs index 4f729320..238fe162 100644 --- a/src/main.rs +++ b/src/main.rs @@ -12,6 +12,7 @@ mod disassemble; mod elf; mod formula_graph; mod iterator; +mod smt; mod solver; mod ternary; @@ -71,6 +72,68 @@ fn main() { Ok(()) }); } + ("smt", Some(_cfg_args)) => { + handle_error(|| -> Result<(), String> { + use crate::{ + dead_code_elimination::eliminate_dead_code, + formula_graph::{build_dataflow_graph, extract_candidate_path}, + }; + use petgraph::dot::Dot; + use std::env::current_dir; + use std::fs::File; + use std::io::Write; + use std::process::Command; + + let cd = String::from(current_dir().unwrap().to_str().unwrap()); + + // generate RISC-U binary with Selfie + let _ = Command::new("docker") + .arg("run") + .arg("-v") + .arg(cd + ":/opt/monster") + .arg("cksystemsteaching/selfie") + .arg("/opt/selfie/selfie") + .arg("-c") + .arg("/opt/monster/symbolic/symbolic-exit.c") + .arg("-o") + .arg("/opt/monster/symbolic/symbolic-exit.riscu.o") + .output(); + + let test_file = Path::new("symbolic/symbolic-exit.riscu.o"); + + let (graph, data_segment, elf_metadata) = cfg::build_from_file(test_file).unwrap(); + + // println!("{:?}", data_segment); + + let (path, branch_decisions) = extract_candidate_path(&graph); + + // println!("{:?}", path); + + let (formula, _root) = build_dataflow_graph( + &path, + data_segment.as_slice(), + elf_metadata, + branch_decisions, + ) + .unwrap(); + + let graph_wo_dc = eliminate_dead_code(&formula, _root); + + let dot_graph = Dot::with_config(&graph_wo_dc, &[]); + + let mut f = File::create("tmp-graph.dot").unwrap(); + f.write_fmt(format_args!("{:?}", dot_graph)).unwrap(); + + let dot_graph = Dot::with_config(&formula, &[]); + + let mut f = File::create("tmp-graph.dot").unwrap(); + f.write_fmt(format_args!("{:?}", dot_graph)).unwrap(); + + smt::smt(&formula); + + Ok(()) + }); + } _ => unreachable!(), } } diff --git a/src/smt.rs b/src/smt.rs new file mode 100644 index 00000000..2c66a0b7 --- /dev/null +++ b/src/smt.rs @@ -0,0 +1,78 @@ +use crate::formula_graph::{ + ArgumentSide, BooleanFunction, Formula, + Node::{Constant, Constraint, Input, Instruction}, +}; +use boolector::{ + option::{BtorOption, ModelGen, OutputFileFormat}, + Btor, BV, +}; +use petgraph::{graph::NodeIndex, Direction}; +use riscv_decode::Instruction as Inst; +use std::rc::Rc; + +fn get_operands( + graph: &Formula, + node: NodeIndex, + solver: &Rc, +) -> (BV>, BV>) { + let mut operands = graph.neighbors_directed(node, Direction::Incoming).detach(); + + match operands.next(graph) { + Some(p) if graph[p.0] == ArgumentSide::Lhs => ( + traverse(graph, p.1, solver), + traverse(graph, operands.next(graph).unwrap().1, solver), + ), + Some(p) if graph[p.0] == ArgumentSide::Rhs => ( + traverse(graph, p.1, solver), + traverse(graph, operands.next(graph).unwrap().1, solver), + ), + _ => unreachable!(), + } +} + +fn traverse<'a>(graph: &Formula, node: NodeIndex, solver: &'a Rc) -> BV> { + match &graph[node] { + Instruction(i) => { + let (lhs, rhs) = get_operands(graph, node, solver); + + match i.instruction { + Inst::Sub(_i) => lhs.sub(&rhs), + Inst::Addi(_i) => lhs.add(&rhs), + Inst::Add(_i) => lhs.add(&rhs), + Inst::Mul(_i) => lhs.mul(&rhs), + Inst::Sltu(_i) => unimplemented!("fix this"), + i => unimplemented!("instruction: {:?}", i), + } + } + Constraint(i) => { + let (lhs, rhs) = get_operands(graph, node, solver); + + match i.op { + BooleanFunction::GreaterThan => lhs.ugt(&rhs), + BooleanFunction::NotEqual => lhs._ne(&rhs), + f => unimplemented!("boolean function: {:?}", f), + } + } + // TODO: use size of read size / 8 + Input(_i) => BV::new(solver.clone(), 8, None), + Constant(i) => BV::from_u64(solver.clone(), i.value, 8), + } +} + +pub fn smt(graph: &Formula) { + graph.externals(Direction::Outgoing).for_each(|n| { + 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)); + + if let Constraint(_) = &graph[n] { + traverse(graph, n, &solver).assert(); + + println!("solver:"); + print!("{}", solver.print_constraints()); + println!("result: {:?}", solver.sat()); + println!(); + } + }); +}