Fix recursion support for shortest path heursitic (#69)

- use consistent names for CLI arguments - move all tests with external dependencies to tests/ (integration test) - refactor integration tests - define feature `pictures` to optionally generate images of CFG's - execute all integration tests in parallel for every source file - rename directory `symbolic` to `examples` closes #69
cksystemsgroup · Nov 12, 2020 · ac52676 · ac52676
1 parent c5c2867
commit ac52676
Show file tree

Hide file tree

Showing 42 changed files with 747 additions and 344 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -5,6 +5,9 @@ authors = ["Christian Mösl <[email protected]>", "Fabian Nedoluha <monste
 edition = "2018"
 description = "Monster is a symbolic execution engine for 64-bit RISC-V code"
 
+[features]
+pictures = [] 
+
 [dependencies]
 goblin = "~0.2.3"
 byteorder = "~1.3.4"
@@ -18,9 +21,11 @@ modinverse = "~0.1.1"
 log = "~0.4.11"
 env_logger = "~0.8.1"
 bytesize = "~1.0.1"
+itertools = "~0.9.0"
 
 [dev-dependencies]
-serial_test = "~0.4.0"
+rayon = "~1.5.0"
+tempfile = "~3.1.0"
 
 [dev-dependencies.cargo-husky]
 version = "1"

diff --git a/symbolic/Cargo.lock → examples/Cargo.lock b/symbolic/Cargo.lock → examples/Cargo.lock
diff --git a/symbolic/Cargo.toml → examples/Cargo.toml b/symbolic/Cargo.toml → examples/Cargo.toml
diff --git a/symbolic/Makefile → examples/Makefile b/symbolic/Makefile → examples/Makefile
diff --git a/symbolic/README.md → examples/README.md b/symbolic/README.md → examples/README.md
diff --git a/symbolic/arithmetic.c → examples/arithmetic.c b/symbolic/arithmetic.c → examples/arithmetic.c
diff --git a/symbolic/division-by-zero-3-35.c → examples/division-by-zero-3-35.c b/symbolic/division-by-zero-3-35.c → examples/division-by-zero-3-35.c
diff --git a/symbolic/division-by-zero-3-35.rs → examples/division-by-zero-3-35.rs b/symbolic/division-by-zero-3-35.rs → examples/division-by-zero-3-35.rs
@@ -9,8 +9,8 @@ Input == #b00110001 (== 49 == '1')
 */
 
 // Pull in the system libc library for what crt0.o likely requires.
-use std::process::exit;
 use std::io::{stdin, Read};
+use std::process::exit;
 
 // Entry point for this program.
 #[allow(unconditional_panic)]
@@ -20,7 +20,7 @@ fn main() {
 
     stdin().read(&mut x);
 
-    x[0] = x[0] - 48;
+    x[0] -= 48;
 
     // division by zero if the input was '0' (== 48)
     let mut a = 41 + (1 / x[0]);
@@ -36,4 +36,3 @@ fn main() {
         exit(0);
     }
 }
-
diff --git a/symbolic/if-else.c → examples/if-else.c b/symbolic/if-else.c → examples/if-else.c
diff --git a/symbolic/invalid-memory-access-2-35.c → examples/invalid-memory-access-2-35.c b/symbolic/invalid-memory-access-2-35.c → examples/invalid-memory-access-2-35.c
diff --git a/symbolic/memory-access-1-35.c → examples/memory-access-1-35.c b/symbolic/memory-access-1-35.c → examples/memory-access-1-35.c
diff --git a/symbolic/nested-if-else-1-35.c → examples/nested-if-else-1-35.c b/symbolic/nested-if-else-1-35.c → examples/nested-if-else-1-35.c
diff --git a/symbolic/nested-if-else-reverse-1-35.c → examples/nested-if-else-reverse-1-35.c b/symbolic/nested-if-else-reverse-1-35.c → examples/nested-if-else-reverse-1-35.c