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

closes #90

examples/endless-loop.c

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

src/cli.rs

@@ -9,6 +9,10 @@ pub fn expect_arg<'a>(m: &'a ArgMatches, arg: &str) -> &'a str {
         .expect(format!("argument \"{}\" has to be set in CLI at all times", arg).as_str())
 }
 
+fn is_u64(v: &str) -> Result<(), String> {
+    v.parse::<u64>().map(|_| ()).map_err(|e| e.to_string())
+}
+
 pub fn args() -> App<'static> {
     App::new(crate_name!())
         .version(crate_version!())
@@ -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 {
+                    extension == "c" && names.into_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,6 +1,6 @@
 mod common;
 
-use common::{compile_all_riscu, init};
+use common::{compile_riscu, init};
 use monster::engine;
 use rayon::prelude::*;
 
@@ -13,22 +13,19 @@ const TEST_FILES: [&str; 6] = [
     "/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();
+        });
+}

tests/exploration_strategy.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::build_cfg_from_file;
 use monster::exploration_strategy::*;
 use petgraph::dot::Dot;
@@ -14,7 +14,7 @@ use std::{
 fn can_build_control_flow_graph_with_distance_from_exit() {
     init();
 
-    compile_all_riscu().1
+    compile_riscu(None).1
         .for_each(|(source_file, object_file)| {
         let ((graph, _), program) = time(format!("compute cfg: {:?}", source_file).as_str(), || {
             build_cfg_from_file(object_file.clone()).unwrap()
@@ -44,12 +44,14 @@ fn can_build_control_flow_graph_with_distance_from_exit() {
         let instructions_in_program = program.code.content.len() / 4;
         let actually = strategy.distances().len() as f64 / instructions_in_program as f64;
 
-        assert!(
-            actually > 0.75,
-            "at least 75% (actually: {:.1}%) of the instructions are reachable and have a distance assigned for: {:?}",
-            actually * 100.0,
-            source_file
-            );
+        if !source_file.ends_with("endless-loop.c") {
+            assert!(
+                actually > 0.75,
+                "at least 75% (actually: {:.1}%) of the instructions are reachable and have a distance assigned for: {:?}",
+                actually * 100.0,
+                source_file
+                );
+        }
 
         if cfg!(feature = "pictures") {
             convert_dot_to_png_and_check(dot_file).unwrap();
@@ -61,7 +63,7 @@ fn can_build_control_flow_graph_with_distance_from_exit() {
 fn can_unroll_procedures_in_control_flow_graph() {
     init();
 
-    compile_all_riscu()
+    compile_riscu(None)
         .1
         .for_each(|(source_file, object_file)| {
             let ((graph, _), program) =