Update LibAFL concolic (#1634)

* concolic upd

* more

* working

* clippy

* rev

* fix

* remove cur_input

* rev

* gitignore

.gitignore

@@ -22,6 +22,7 @@ vendor
 
 .cur_input
 .cur_input_*
+cur_input
 .venv
 
 crashes
@@ -60,3 +61,8 @@ libafl_nyx/QEMU-Nyx
 libafl_nyx/packer
 
 .z3-trace
+
+# No gdb history
+.gdb_history
+# No llvm IR
+*.ll

fuzzers/libfuzzer_stb_image_concolic/Makefile.toml

@@ -51,6 +51,9 @@ clear = true
 script='''
 cd fuzzer 
 cargo clean
-cd ../runtime
+cd ..
+cd ./runtime
+cargo clean
+cd ..
 cargo clean
 '''

fuzzers/libfuzzer_stb_image_concolic/fuzzer/src/main.rs

@@ -60,13 +60,14 @@ struct Opt {
     concolic: bool,
 }
 
+use std::fs;
 pub fn main() {
     // Registry the metadata types used in this fuzzer
     // Needed only on no_std
     // unsafe { RegistryBuilder::register::<Tokens>(); }
 
     let opt = Opt::parse();
-
+    let _ = fs::remove_file("cur_input");
     println!(
         "Workdir: {:?}",
         env::current_dir().unwrap().to_string_lossy().to_string()

libafl/src/observers/concolic/mod.rs

@@ -252,7 +252,9 @@ pub enum SymExpr {
         a: SymExprRef,
         b: SymExprRef,
     },
-
+    FloatNeg {
+        op: SymExprRef,
+    },
     FloatAbs {
         op: SymExprRef,
     },
@@ -277,6 +279,11 @@ pub enum SymExpr {
         b: SymExprRef,
     },
 
+    Ite {
+        cond: SymExprRef,
+        a: SymExprRef,
+        b: SymExprRef,
+    },
     Sext {
         op: SymExprRef,
         bits: u8,

libafl/src/observers/concolic/serialization_format.rs

@@ -110,6 +110,7 @@ impl<R: Read> MessageFileReader<R> {
 
     /// This transforms the given message from it's serialized form into its in-memory form, making relative references
     /// absolute and counting the `SymExprRef`s.
+    #[allow(clippy::too_many_lines)]
     fn transform_message(&mut self, message: &mut SymExpr) -> SymExprRef {
         let ret = self.current_id;
         match message {
@@ -125,6 +126,7 @@ impl<R: Read> MessageFileReader<R> {
             }
             SymExpr::Neg { op }
             | SymExpr::FloatAbs { op }
+            | SymExpr::FloatNeg { op }
             | SymExpr::Not { op }
             | SymExpr::Sext { op, .. }
             | SymExpr::Zext { op, .. }
@@ -204,6 +206,12 @@ impl<R: Read> MessageFileReader<R> {
                 }
             }
             SymExpr::Call { .. } | SymExpr::Return { .. } | SymExpr::BasicBlock { .. } => {}
+            SymExpr::Ite { cond, a, b } => {
+                *cond = self.make_absolute(*cond);
+                *a = self.make_absolute(*a);
+                *b = self.make_absolute(*b);
+                self.current_id += 1;
+            }
         }
         SymExprRef::new(ret).unwrap()
     }
@@ -291,6 +299,7 @@ impl<W: Write + Seek> MessageFileWriter<W> {
             }
             SymExpr::Neg { op }
             | SymExpr::FloatAbs { op }
+            | SymExpr::FloatNeg { op }
             | SymExpr::Not { op }
             | SymExpr::Sext { op, .. }
             | SymExpr::Zext { op, .. }
@@ -370,6 +379,11 @@ impl<W: Write + Seek> MessageFileWriter<W> {
                 }
             }
             SymExpr::Call { .. } | SymExpr::Return { .. } | SymExpr::BasicBlock { .. } => {}
+            SymExpr::Ite { cond, a, b } => {
+                *cond = self.make_relative(*cond);
+                *a = self.make_relative(*a);
+                *b = self.make_relative(*b);
+            }
         }
         self.serialization_options
             .serialize_into(&mut self.writer, &message)?;

libafl_concolic/symcc_libafl/src/lib.rs

@@ -5,7 +5,7 @@
 /// The URL of the `LibAFL` `SymCC` fork.
 pub const SYMCC_REPO_URL: &str = "https://github.com/AFLplusplus/symcc.git";
 /// The commit of the `LibAFL` `SymCC` fork.
-pub const SYMCC_REPO_COMMIT: &str = "2a3229da6101596af220f20fef5085e59537abcb";
+pub const SYMCC_REPO_COMMIT: &str = "6909c3f2b98c6e14a25bee0fc6eb29c598250e35";
 
 #[cfg(feature = "clone")]
 mod clone {

libafl_concolic/symcc_runtime/src/filter.rs

@@ -240,4 +240,7 @@ impl Filter for NoFloat {
     fn build_fp_rem(&mut self, _a: RSymExpr, _b: RSymExpr) -> bool {
         false
     }
+    fn build_fp_neg(&mut self, _a: RSymExpr) -> bool {
+        false
+    }
 }

libafl_concolic/symcc_runtime/src/tracing.rs

@@ -127,6 +127,7 @@ impl Runtime for TracingRuntime {
     binary_expression_builder!(build_fp_rem, FloatRem);
 
     unary_expression_builder!(build_fp_abs, FloatAbs);
+    unary_expression_builder!(build_fp_neg, FloatNeg);
 
     unary_expression_builder!(build_not, Not);
     binary_expression_builder!(build_equal, Equal);
@@ -135,6 +136,7 @@ impl Runtime for TracingRuntime {
     binary_expression_builder!(build_bool_or, BoolOr);
     binary_expression_builder!(build_bool_xor, BoolXor);
 
+    expression_builder!(build_ite(cond: RSymExpr, a: RSymExpr, b: RSymExpr) => Ite);
     expression_builder!(build_sext(op: RSymExpr, bits: u8) => Sext);
     expression_builder!(build_zext(op: RSymExpr, bits: u8) => Zext);
     expression_builder!(build_trunc(op: RSymExpr, bits: u8) => Trunc);