From 948c94d6956e698e369814373c25c25e8af354a7 Mon Sep 17 00:00:00 2001 From: julihoh Date: Sat, 19 Nov 2022 23:05:15 +0100 Subject: [PATCH] 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 | 4 ++-- libafl/src/observers/concolic/serialization_format.rs | 9 ++++++--- libafl/src/stages/concolic.rs | 9 +++------ libafl_concolic/symcc_libafl/src/lib.rs | 2 +- libafl_concolic/symcc_runtime/src/filter.rs | 4 ++-- libafl_concolic/symcc_runtime/src/tracing.rs | 4 ++-- libafl_concolic/test/expected_constraints.txt | 8 ++++---- libafl_concolic/test/smoke_test.sh | 9 +++------ 8 files changed, 23 insertions(+), 26 deletions(-) diff --git a/libafl/src/observers/concolic/mod.rs b/libafl/src/observers/concolic/mod.rs index 115c39082a..a3a4bbc42e 100644 --- a/libafl/src/observers/concolic/mod.rs +++ b/libafl/src/observers/concolic/mod.rs @@ -58,6 +58,7 @@ impl From 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 { diff --git a/libafl/src/observers/concolic/serialization_format.rs b/libafl/src/observers/concolic/serialization_format.rs index 4ea6cf1615..9e1497128b 100644 --- a/libafl/src/observers/concolic/serialization_format.rs +++ b/libafl/src/observers/concolic/serialization_format.rs @@ -135,7 +135,7 @@ impl MessageFileReader { | 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 MessageFileWriter { // 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 MessageFileWriter { | 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; diff --git a/libafl/src/stages/concolic.rs b/libafl/src/stages/concolic.rs index e711f21ab2..3332c52752 100644 --- a/libafl/src/stages/concolic.rs +++ b/libafl/src/stages/concolic.rs @@ -157,7 +157,7 @@ fn generate_mutations(iter: impl Iterator) -> Vec< for (id, msg) in iter { let z3_expr: Option = 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) -> 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( - &BV::from_u64(&ctx, 1, u32::from(bits)), - &BV::from_u64(&ctx, 0, u32::from(bits)), - ) + .ite(&BV::from_u64(&ctx, 1, 1), &BV::from_u64(&ctx, 0, 1)) .into(), ), SymExpr::Concat { a, b } => bv_binop!(a concat b), diff --git a/libafl_concolic/symcc_libafl/src/lib.rs b/libafl_concolic/symcc_libafl/src/lib.rs index 013b8a6ed7..f5a1e0e9e5 100644 --- a/libafl_concolic/symcc_libafl/src/lib.rs +++ 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 { diff --git a/libafl_concolic/symcc_runtime/src/filter.rs b/libafl_concolic/symcc_runtime/src/filter.rs index 17d6b4cce2..74740d3ff9 100644 --- a/libafl_concolic/symcc_runtime/src/filter.rs +++ b/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) } } diff --git a/libafl_concolic/symcc_runtime/src/tracing.rs b/libafl_concolic/symcc_runtime/src/tracing.rs index 3919dc9879..51186e903b 100644 --- a/libafl_concolic/symcc_runtime/src/tracing.rs +++ b/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); diff --git a/libafl_concolic/test/expected_constraints.txt b/libafl_concolic/test/expected_constraints.txt index 7b4f961e63..2efb226203 100644 --- a/libafl_concolic/test/expected_constraints.txt +++ b/libafl_concolic/test/expected_constraints.txt @@ -1,7 +1,7 @@ -1 InputByte { offset: 0 } -2 InputByte { offset: 1 } -3 InputByte { offset: 2 } -4 InputByte { offset: 3 } +1 InputByte { offset: 0, value: 49 } +2 InputByte { offset: 1, value: 50 } +3 InputByte { offset: 2, value: 51 } +4 InputByte { offset: 3, value: 52 } 5 Concat { a: 2, b: 1 } 6 Concat { a: 3, b: 5 } 7 Concat { a: 4, b: 6 } diff --git a/libafl_concolic/test/smoke_test.sh b/libafl_concolic/test/smoke_test.sh index 1d4eb08977..4e23543e9e 100755 --- a/libafl_concolic/test/smoke_test.sh +++ b/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" -cargo build -p runtime_test - -echo "building dump_constraints" -cargo build -p dump_constraints +echo "building runtime and dump_constraints" +cargo build -p runtime_test -p dump_constraints echo "building target" SYMCC_RUNTIME_DIR=../../target/debug symcc_build/symcc symcc/test/if.c -o "if"