Update and fix concolic support (#901)

* fix incorrect assert condition and document it

* update symcc

* adapt to changes in symcc API

* more fixes

* fix formatting

* more fixes

* speed up smoke test by building multiple crates in one command

* update symcc commit to latest main

libafl/src/observers/concolic/mod.rs

@@ -58,6 +58,7 @@ impl From<usize> for Location {
 pub enum SymExpr {
     InputByte {
         offset: usize,
+        value: u8,
     },
 
     Integer {
@@ -312,9 +313,8 @@ pub enum SymExpr {
         op: SymExprRef,
         bits: u8,
     },
-    BoolToBits {
+    BoolToBit {
         op: SymExprRef,
-        bits: u8,
     },
 
     Concat {

libafl/src/observers/concolic/serialization_format.rs

@@ -135,7 +135,7 @@ impl<R: Read> MessageFileReader<R> {
             | SymExpr::FloatToBits { op }
             | SymExpr::FloatToSignedInteger { op, .. }
             | SymExpr::FloatToUnsignedInteger { op, .. }
-            | SymExpr::BoolToBits { op, .. }
+            | SymExpr::BoolToBit { op, .. }
             | SymExpr::Extract { op, .. } => {
                 *op = self.make_absolute(*op);
                 self.current_id += 1;
@@ -248,7 +248,10 @@ impl<W: Write + Seek> MessageFileWriter<W> {
         // calculate size of trace
         let end_pos = self.writer.stream_position()?;
         let trace_header_len = 0_u64.to_le_bytes().len() as u64;
-        assert!(end_pos > self.writer_start_position + trace_header_len);
+        assert!(
+            end_pos >= self.writer_start_position + trace_header_len,
+            "our end position can not be before our start position"
+        );
         let trace_length = end_pos - self.writer_start_position - trace_header_len;
 
         // write trace size to beginning of trace
@@ -298,7 +301,7 @@ impl<W: Write + Seek> MessageFileWriter<W> {
             | SymExpr::FloatToBits { op }
             | SymExpr::FloatToSignedInteger { op, .. }
             | SymExpr::FloatToUnsignedInteger { op, .. }
-            | SymExpr::BoolToBits { op, .. }
+            | SymExpr::BoolToBit { op, .. }
             | SymExpr::Extract { op, .. } => {
                 *op = self.make_relative(*op);
                 self.id_counter += 1;

libafl/src/stages/concolic.rs

@@ -157,7 +157,7 @@ fn generate_mutations(iter: impl Iterator<Item = (SymExprRef, SymExpr)>) -> Vec<
 
     for (id, msg) in iter {
         let z3_expr: Option<Dynamic> = match msg {
-            SymExpr::InputByte { offset } => {
+            SymExpr::InputByte { offset, .. } => {
                 Some(BV::new_const(&ctx, Symbol::Int(offset as u32), 8).into())
             }
             SymExpr::Integer { value, bits } => {
@@ -211,12 +211,9 @@ fn generate_mutations(iter: impl Iterator<Item = (SymExprRef, SymExpr)>) -> Vec<
             SymExpr::Sext { op, bits } => Some(bv!(op).sign_ext(u32::from(bits)).into()),
             SymExpr::Zext { op, bits } => Some(bv!(op).zero_ext(u32::from(bits)).into()),
             SymExpr::Trunc { op, bits } => Some(bv!(op).extract(u32::from(bits - 1), 0).into()),
-            SymExpr::BoolToBits { op, bits } => Some(
+            SymExpr::BoolToBit { op } => Some(
                 bool!(op)
-                    .ite(
+                    .ite(&BV::from_u64(&ctx, 1, 1), &BV::from_u64(&ctx, 0, 1))
-                        &BV::from_u64(&ctx, 1, u32::from(bits)),
-                        &BV::from_u64(&ctx, 0, u32::from(bits)),
-                    )
                     .into(),
             ),
             SymExpr::Concat { a, b } => bv_binop!(a concat b),

libafl_concolic/symcc_libafl/src/lib.rs

@@ -4,7 +4,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 = "5cccc33456c48ad83008eb618e7da5d005c72d89";
+pub const SYMCC_REPO_COMMIT: &str = "2a3229da6101596af220f20fef5085e59537abcb";
 
 #[cfg(feature = "clone")]
 mod clone {

libafl_concolic/symcc_runtime/src/filter.rs

@@ -68,7 +68,7 @@ macro_rules! rust_filter_function_declaration {
 /// }
 ///
 /// impl Filter for SelectiveSymbolication {
-///     fn get_input_byte(&mut self, offset: usize) -> bool {
+///     fn get_input_byte(&mut self, offset: usize, value: u8) -> bool {
 ///         self.bytes_to_symbolize.contains(&offset)
 ///     }
 ///     // Note: No need to implement methods that we are not interested in!
@@ -150,7 +150,7 @@ impl SelectiveSymbolication {
 }
 
 impl Filter for SelectiveSymbolication {
-    fn get_input_byte(&mut self, offset: usize) -> bool {
+    fn get_input_byte(&mut self, offset: usize, _value: u8) -> bool {
         self.bytes_to_symbolize.contains(&offset)
     }
 }

libafl_concolic/symcc_runtime/src/tracing.rs

@@ -62,7 +62,7 @@ macro_rules! binary_expression_builder {
 }
 
 impl Runtime for TracingRuntime {
-    expression_builder!(get_input_byte(offset: usize) => InputByte);
+    expression_builder!(get_input_byte(offset: usize, value: u8) => InputByte);
 
     expression_builder!(build_integer(value: u64, bits: u8) => Integer);
     expression_builder!(build_integer128(high: u64, low: u64) => Integer128);
@@ -144,7 +144,7 @@ impl Runtime for TracingRuntime {
     expression_builder!(build_float_to_bits(op: RSymExpr) => FloatToBits);
     expression_builder!(build_float_to_signed_integer(op: RSymExpr, bits: u8) => FloatToSignedInteger);
     expression_builder!(build_float_to_unsigned_integer(op: RSymExpr, bits: u8) => FloatToUnsignedInteger);
-    expression_builder!(build_bool_to_bits(op: RSymExpr, bits: u8) => BoolToBits);
+    expression_builder!(build_bool_to_bit(op: RSymExpr) => BoolToBit);
 
     binary_expression_builder!(concat_helper, Concat);
     expression_builder!(extract_helper(op: RSymExpr, first_bit:usize, last_bit:usize) => Extract);

libafl_concolic/test/expected_constraints.txt

@@ -1,7 +1,7 @@
-1	InputByte { offset: 0 }
+1	InputByte { offset: 0, value: 49 }
-2	InputByte { offset: 1 }
+2	InputByte { offset: 1, value: 50 }
-3	InputByte { offset: 2 }
+3	InputByte { offset: 2, value: 51 }
-4	InputByte { offset: 3 }
+4	InputByte { offset: 3, value: 52 }
 5	Concat { a: 2, b: 1 }
 6	Concat { a: 3, b: 5 }
 7	Concat { a: 4, b: 6 }

libafl_concolic/test/smoke_test.sh

@@ -16,7 +16,7 @@ if [ ! -d "symcc" ]; then
     echo "cloning symcc"
     git clone https://github.com/AFLplusplus/symcc.git symcc
     cd symcc
-    git checkout 5cccc33456c48ad83008eb618e7da5d005c72d89
+    git checkout 2a3229da6101596af220f20fef5085e59537abcb
     cd ..
 fi
 
@@ -30,11 +30,8 @@ if [ ! -d "symcc_build" ]; then
 fi
 
 
-echo "building runtime"
+echo "building runtime and dump_constraints"
-cargo build -p runtime_test
+cargo build -p runtime_test -p dump_constraints
-
-echo "building dump_constraints"
-cargo build -p dump_constraints
 
 echo "building target"
 SYMCC_RUNTIME_DIR=../../target/debug symcc_build/symcc symcc/test/if.c -o "if"