feat: add "execution depth" as abort criteria (#90)

closes #90

Cargo.toml

@@ -12,7 +12,7 @@ pictures = []
 goblin = "~0.2.3"
 byteorder = "~1.3.4"
 clap = "3.0.0-beta.2"
-riscu = "~0.3.1"
+riscu = "~0.3.2"
 petgraph = "~0.5.1"
 rand = "~0.7.3"
 boolector = { version = "0.4", git = "https://github.com/finga/boolector-rs", branch = "boolector-src", features = ["vendored"] }

examples/endless-loop.c

@@ -0,0 +1,10 @@
+uint64_t main() {
+  uint64_t  i;
+
+  i = 1;
+
+  while (i == 1) {
+  }
+
+  return 0;
+}

src/cfg.rs

@@ -49,9 +49,8 @@ fn create_instruction_graph(binary: &[u8]) -> Result<ControlFlowGraph> {
         .chunks_exact(size_of::<u32>())
         .map(LittleEndian::read_u32)
         .try_for_each(|raw| {
-            decode(raw).and_then(|i| {
+            decode(raw).map(|i| {
                 g.add_node(i);
-                Ok(())
             })
         })?;
 
@@ -211,7 +210,7 @@ fn fix_exit_ecall(graph: &mut ControlFlowGraph) -> Result<NodeIndex> {
             }
             false
         })
-        .ok_or(Error::msg("Could not find exit ecall in binary"))
+        .ok_or_else(|| Error::msg("Could not find exit ecall in binary"))
 }
 
 /// Create a ControlFlowGraph from `u8` slice.

src/cli.rs

@@ -6,7 +6,11 @@ pub const SOLVER: [&str; 3] = ["monster", "boolector", "z3"];
 
 pub fn expect_arg<'a>(m: &'a ArgMatches, arg: &str) -> &'a str {
     m.value_of(arg)
-        .expect(format!("argument \"{}\" has to be set in CLI at all times", arg).as_str())
+        .unwrap_or_else(|| panic!("argument \"{}\" has to be set in CLI at all times", arg))
+}
+
+fn is_u64(v: &str) -> Result<(), String> {
+    v.parse::<u64>().map(|_| ()).map_err(|e| e.to_string())
 }
 
 pub fn args() -> App<'static> {
@@ -22,15 +26,14 @@ pub fn args() -> App<'static> {
                 .takes_value(true)
                 .value_name("LEVEL")
                 .possible_values(&LOGGING_LEVELS)
-                .default_value(LOGGING_LEVELS[2]),
+                .default_value(LOGGING_LEVELS[2])
+                .global(true),
         )
         .subcommand(
             App::new("disassemble")
                 .about("Disassemble a RISC-V ELF binary")
                 .arg(
                     Arg::new("input-file")
-                        .short('c')
-                        .long("disassemble")
                         .value_name("FILE")
                         .about("Binary file to be disassembled")
                         .takes_value(true)
@@ -43,8 +46,6 @@ pub fn args() -> App<'static> {
                 .arg(
                     Arg::new("input-file")
                         .about("Source RISC-U binary to be analyzed")
-                        .short('f')
-                        .long("file")
                         .takes_value(true)
                         .value_name("FILE")
                         .required(true),
@@ -71,8 +72,6 @@ pub fn args() -> App<'static> {
                 .arg(
                     Arg::new("input-file")
                         .about("RISC-U ELF binary to be executed")
-                        .short('f')
-                        .long("file")
                         .takes_value(true)
                         .value_name("FILE")
                         .required(true),
@@ -83,8 +82,18 @@ pub fn args() -> App<'static> {
                         .short('s')
                         .long("solver")
                         .takes_value(true)
+                        .value_name("SOLVER")
                         .possible_values(&SOLVER)
                         .default_value(SOLVER[0]),
+                )
+                .arg(
+                    Arg::new("max-execution-depth")
+                        .about("Number of instructions, where the path execution will be aborted")
+                        .short('d')
+                        .long("execution-depth")
+                        .takes_value(true)
+                        .value_name("NUMBER")
+                        .validator(is_u64),
                 ),
         )
         .setting(AppSettings::SubcommandRequiredElseHelp)

src/engine.rs

@@ -30,7 +30,7 @@ pub enum Backend {
 }
 
 // TODO: What should the engine return as result?
-pub fn execute<P>(input: P, with: Backend) -> Result<()>
+pub fn execute<P>(input: P, with: Backend, max_exection_depth: u64) -> Result<()>
 where
     P: AsRef<Path>,
 {
@@ -43,23 +43,41 @@ where
             let solver = Rc::new(RefCell::new(MonsterSolver::new()));
             let state = Box::new(SymbolicState::new(solver));
 
-            let mut executor = Engine::new(ByteSize::mib(1), &program, &mut strategy, state);
+            let mut executor = Engine::new(
+                ByteSize::mib(1),
+                max_exection_depth,
+                &program,
+                &mut strategy,
+                state,
+            );
 
             executor.run()
         }
         Backend::Boolector => {
             let solver = Rc::new(RefCell::new(Boolector::new()));
             let state = Box::new(SymbolicState::new(solver));
 
-            let mut executor = Engine::new(ByteSize::mib(1), &program, &mut strategy, state);
+            let mut executor = Engine::new(
+                ByteSize::mib(1),
+                max_exection_depth,
+                &program,
+                &mut strategy,
+                state,
+            );
 
             executor.run()
         }
         Backend::Z3 => {
             let solver = Rc::new(RefCell::new(Z3::new()));
             let state = Box::new(SymbolicState::new(solver));
 
-            let mut executor = Engine::new(ByteSize::mib(1), &program, &mut strategy, state);
+            let mut executor = Engine::new(
+                ByteSize::mib(1),
+                max_exection_depth,
+                &program,
+                &mut strategy,
+                state,
+            );
 
             executor.run()
         }
@@ -94,6 +112,8 @@ where
     regs: [Value; 32],
     memory: Vec<Value>,
     strategy: &'a mut E,
+    execution_depth: u64,
+    max_exection_depth: u64,
     is_exited: bool,
 }
 
@@ -105,6 +125,7 @@ where
     // creates a machine state with a specific memory size
     pub fn new(
         memory_size: ByteSize,
+        max_exection_depth: u64,
         program: &Program,
         strategy: &'a mut E,
         symbolic_state: Box<SymbolicState<S>>,
@@ -152,6 +173,8 @@ where
             regs,
             memory,
             strategy,
+            execution_depth: 0,
+            max_exection_depth,
             is_exited: false,
         }
     }
@@ -170,6 +193,16 @@ where
 
     pub fn run(&mut self) -> Result<()> {
         while !self.is_exited {
+            if self.execution_depth >= self.max_exection_depth {
+                trace!("maximum execution depth reached => exiting this context");
+
+                self.is_exited = true;
+
+                break;
+            }
+
+            self.execution_depth += 1;
+
             let word = self.fetch();
 
             let instr = decode(word)?;

src/main.rs

@@ -47,6 +47,9 @@ fn main() -> Result<()> {
         Some(("execute", args)) => {
             let input = Path::new(expect_arg(&args, "input-file"));
             let solver = expect_arg(&args, "solver");
+            let depth = args
+                .value_of_t::<u64>("max-execution-depth")
+                .expect("value is validated already");
 
             engine::execute(
                 input,
@@ -56,6 +59,7 @@ fn main() -> Result<()> {
                     "z3" => engine::Backend::Z3,
                     _ => unreachable!(),
                 },
+                depth,
             )
         }
         _ => unreachable!(),

tests/cfg.rs

@@ -1,6 +1,6 @@
 mod common;
 
-use common::{compile_all_riscu, convert_dot_to_png_and_check, init, time};
+use common::{compile_riscu, convert_dot_to_png_and_check, init, time};
 use monster::cfg::*;
 use petgraph::dot::Dot;
 use rayon::prelude::*;
@@ -10,7 +10,7 @@ use std::{fs::File, io::prelude::*};
 fn can_build_control_flow_graph() {
     init();
 
-    compile_all_riscu().1.for_each(|(source, object)| {
+    compile_riscu(None).1.for_each(|(source, object)| {
         let ((graph, _), _) = time(format!("compute cfg: {:?}", source).as_str(), || {
             build_cfg_from_file(object.clone()).unwrap()
         });

tests/common.rs

@@ -102,7 +102,9 @@ where
     result
 }
 
-pub fn compile_all_riscu() -> (
+pub fn compile_riscu(
+    filter: Option<&'static [&str]>,
+) -> (
     Arc<TempDir>,
     impl ParallelIterator<Item = (PathBuf, PathBuf)>,
 ) {
@@ -113,9 +115,13 @@ pub fn compile_all_riscu() -> (
         .unwrap()
         .par_bridge()
         .map(|dir_entry| dir_entry.unwrap().path())
-        .filter(|path| {
+        .filter(move |path| {
             if let Some(extension) = path.extension() {
-                extension == "c"
+                if let Some(names) = filter {
+                    names.iter().any(|name| path.ends_with(name))
+                } else {
+                    extension == "c"
+                }
             } else {
                 false
             }
@@ -126,7 +132,7 @@ pub fn compile_all_riscu() -> (
                 .join(source_file.with_extension("o").file_name().unwrap());
 
             let result_path = time(
-                format!("compile: {}", source_file.to_str().unwrap()).as_str(),
+                format!("compile: {}", source_file.display()).as_str(),
                 || compile(source_file.clone(), dst_file_path.clone()).unwrap(),
             );
 

tests/disassemble.rs

@@ -1,14 +1,14 @@
 mod common;
 
-use common::{compile_all_riscu, init};
+use common::{compile_riscu, init};
 use monster::disassemble::*;
 use rayon::prelude::*;
 
 #[test]
 fn can_disassemble_risc_u_binary() {
     init();
 
-    compile_all_riscu().1.for_each(|(source, object)| {
+    compile_riscu(None).1.for_each(|(source, object)| {
         let result = disassemble(object);
 
         assert!(

tests/engine.rs

@@ -1,34 +1,31 @@
 mod common;
 
-use common::{compile_all_riscu, init};
+use common::{compile_riscu, init};
 use monster::engine;
 use rayon::prelude::*;
 
 const TEST_FILES: [&str; 6] = [
-    "/arithmetic.c",
-    "/if-else.c",
-    "/invalid-memory-access-2-35.c",
-    "/division-by-zero-3-35.c",
-    "/simple-assignment-1-35.c",
-    "/test-sltu.c",
+    "arithmetic.c",
+    "if-else.c",
+    "invalid-memory-access-2-35.c",
+    "division-by-zero-3-35.c",
+    "simple-assignment-1-35.c",
+    "test-sltu.c",
 ];
 
-fn execute_riscu(names: &[&str], solver: engine::Backend) {
+fn execute_riscu(names: &'static [&str], solver: engine::Backend) {
     init();
-    compile_all_riscu()
-        .1
-        .filter(|(source, _)| names.iter().any(|name| source.ends_with(name)))
-        .for_each(|(source, object)| {
-            let result = engine::execute(object, solver);
-
-            assert!(
-                result.is_ok(),
-                format!(
-                    "can symbolically execute '{}' without error",
-                    source.to_str().unwrap()
-                )
-            );
-        });
+    compile_riscu(Some(names)).1.for_each(|(source, object)| {
+        let result = engine::execute(object, solver, 100000);
+
+        assert!(
+            result.is_ok(),
+            format!(
+                "can symbolically execute '{}' without error",
+                source.to_str().unwrap()
+            )
+        );
+    });
 }
 
 #[test]
@@ -45,3 +42,14 @@ fn execute_riscu_with_boolector_solver() {
 fn execute_riscu_with_z3_solver() {
     execute_riscu(&TEST_FILES, engine::Backend::Z3);
 }
+
+#[test]
+fn execute_engine_for_endless_loops() {
+    init();
+
+    compile_riscu(Some(&["endless-loop.c"]))
+        .1
+        .for_each(|(_, object)| {
+            engine::execute(object, engine::Backend::Monster, 5).unwrap();
+        });
+}