Concolic example fuzzer fixes (#251)

* fix compilation of runtime of concolic example fuzzer

* fix compilation of example fuzzer

* fix incorrect traced target configuration

this would lead to the runtime never tracing any expressions.
failed to specifiy the input file name for the runtime to know what to symbolize

* add ability to specify whether a node should do concolic or traditional

* slightly more realistic concolic solving by using solver timeout

* enable expression pruning

fuzzers/libfuzzer_stb_image_concolic/fuzzer/Cargo.toml

@@ -18,6 +18,7 @@ debug = true
 [dependencies]
 libafl = { path = "../../../libafl/", features = ["concolic_mutation"] }
 libafl_targets = { path = "../../../libafl_targets/", features = ["sancov_pcguard_edges", "sancov_cmplog", "libfuzzer"] }
+structopt = "0.3.21"
 
 [build-dependencies]
 cc = { version = "1.0", features = ["parallel"] }

fuzzers/libfuzzer_stb_image_concolic/fuzzer/src/main.rs

@@ -28,7 +28,7 @@ use libafl::{
     },
     observers::{
         concolic::{
-            serialization_format::shared_memory::{DEFAULT_ENV_NAME, DEFAULT_SIZE},
+            serialization_format::{DEFAULT_ENV_NAME, DEFAULT_SIZE},
             ConcolicObserver,
         },
         StdMapObserver, TimeObserver,
@@ -47,11 +47,22 @@ use libafl_targets::{
     MAX_EDGES_NUM,
 };
 
+use structopt::StructOpt;
+
+#[derive(Debug, StructOpt)]
+struct Opt {
+    /// This node should do concolic tracing + solving instead of traditional fuzzing
+    #[structopt(short, long)]
+    concolic: bool,
+}
+
 pub fn main() {
     // Registry the metadata types used in this fuzzer
     // Needed only on no_std
     //RegistryBuilder::register::<Tokens>();
 
+    let opt = Opt::from_args();
+
     println!(
         "Workdir: {:?}",
         env::current_dir().unwrap().to_string_lossy().to_string()
@@ -60,12 +71,18 @@ pub fn main() {
         &[PathBuf::from("./corpus")],
         PathBuf::from("./crashes"),
         1337,
+        opt.concolic,
     )
     .expect("An error occurred while fuzzing");
 }
 
 /// The actual fuzzer
-fn fuzz(corpus_dirs: &[PathBuf], objective_dir: PathBuf, broker_port: u16) -> Result<(), Error> {
+fn fuzz(
+    corpus_dirs: &[PathBuf],
+    objective_dir: PathBuf,
+    broker_port: u16,
+    concolic: bool,
+) -> Result<(), Error> {
     // 'While the stats are state, they are usually used in the broker - which is likely never restarted
     let stats = MultiStats::new(|s| println!("{}", s));
 
@@ -183,6 +200,7 @@ fn fuzz(corpus_dirs: &[PathBuf], objective_dir: PathBuf, broker_port: u16) -> Re
     let mutator = StdScheduledMutator::new(havoc_mutations());
     let mutational = StdMutationalStage::new(mutator);
 
+    if concolic {
         // The shared memory for the concolic runtime to write its trace to
         let mut concolic_shmem = StdShMemProvider::new()
             .unwrap()
@@ -191,7 +209,8 @@ fn fuzz(corpus_dirs: &[PathBuf], objective_dir: PathBuf, broker_port: u16) -> Re
         concolic_shmem.write_to_env(DEFAULT_ENV_NAME).unwrap();
 
         // The concolic observer observers the concolic shared memory map.
-    let concolic_observer = ConcolicObserver::new("concolic".to_string(), concolic_shmem.map_mut());
+        let concolic_observer =
+            ConcolicObserver::new("concolic".to_string(), concolic_shmem.map_mut());
 
         let concolic_observer_name = concolic_observer.name().to_string();
 
@@ -206,12 +225,15 @@ fn fuzz(corpus_dirs: &[PathBuf], objective_dir: PathBuf, broker_port: u16) -> Re
             ),
             // Use the concolic trace for z3-based solving
             SimpleConcolicMutationalStage::default(),
-        tracing,
-        i2s,
-        mutational
         );
 
         fuzzer.fuzz_loop(&mut stages, &mut executor, &mut state, &mut restarting_mgr)?;
+    } else {
+        // The order of the stages matter!
+        let mut stages = tuple_list!(tracing, i2s, mutational);
+
+        fuzzer.fuzz_loop(&mut stages, &mut executor, &mut state, &mut restarting_mgr)?;
+    }
 
     // Never reached
     Ok(())
@@ -240,6 +262,7 @@ where
             .stdin(Stdio::null())
             .stdout(Stdio::null())
             .stderr(Stdio::null())
+            .env("SYMCC_INPUT_FILE", "cur_input")
             .spawn()
             .expect("failed to start process"))
     }

fuzzers/libfuzzer_stb_image_concolic/runtime/src/lib.rs

@@ -1,17 +1,18 @@
-use symcc_runtime::{
-    export_runtime,
-    filter::NoFloat,
-    tracing::{self, StdShMemMessageFileWriter},
-    Runtime,
-};
-
 //! This is a basic SymCC runtime.
 //! It traces the execution to the shared memory region that should be passed through the environment by the fuzzer process. 
 //! Additionally, it concretizes all floating point operations for simplicity.
 //! Refer to the `symcc_runtime` crate documentation for building your own runtime.
 
+use symcc_runtime::{
+    export_runtime,
+    filter::{NoFloat, CallStackCoverage},
+    tracing::{self, StdShMemMessageFileWriter},
+    Runtime,
+};
+
 export_runtime!(
     NoFloat => NoFloat;
+    CallStackCoverage::default() => CallStackCoverage; // QSym-style expression pruning
     tracing::TracingRuntime::new(
         StdShMemMessageFileWriter::from_stdshmem_default_env()
             .expect("unable to construct tracing runtime writer. (missing env?)")

libafl/src/stages/concolic.rs

@@ -134,7 +134,9 @@ fn generate_mutations(iter: impl Iterator<Item = (SymExprRef, SymExpr)>) -> Vec<
 
     let mut res = Vec::new();
 
-    let ctx = Context::new(&Config::new());
+    let mut cfg = Config::new();
+    cfg.set_timeout_msec(10_000);
+    let ctx = Context::new(&cfg);
     let solver = Solver::new(&ctx);
 
     let mut translation = HashMap::<SymExprRef, Dynamic>::new();
@@ -305,7 +307,6 @@ fn generate_mutations(iter: impl Iterator<Item = (SymExprRef, SymExpr)>) -> Vec<
                     }
                     z3::SatResult::Unknown => {
                         // we've got a problem. ignore
-                        solver.pop(1);
                     }
                     z3::SatResult::Sat => {
                         let model = solver.get_model().unwrap();