feat: add smt generation and solving (#38)

Use the patched `boolector-sys` crate for now. This closes #16.

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"

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)
 }

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,64 +616,62 @@ 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<Instruction>, Vec<bool>) {
+    fn next(graph: &ControlFlowGraph, idx: NodeIndex) -> Option<(NodeIndex, Option<bool>)> {
+        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;
     use std::io::prelude::*;
     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<Instruction>, Vec<bool>) {
-        fn next(graph: &ControlFlowGraph, idx: NodeIndex) -> Option<(NodeIndex, Option<bool>)> {
-            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]

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!(),
     }
 }