Documentation and Refactors for Concolic (#243)
* document symcc_runtime * rename serialization format expressions to be more concise * authorship notes * document dump_constraints * document smoke test * tests for serialization format and refactoring * remove unused bswap message * remove obselete SymExpr::End * document and refactor serialization format * fmt * more missing docs * typos * clippy
This commit is contained in:
parent
3d98d31712
commit
704830a501
@ -2,6 +2,7 @@
|
|||||||
name = "example_runtime"
|
name = "example_runtime"
|
||||||
version = "0.1.0"
|
version = "0.1.0"
|
||||||
edition = "2018"
|
edition = "2018"
|
||||||
|
authors = ["Julius Hohnerlein <julihoh@users.noreply.github.com>"]
|
||||||
|
|
||||||
[lib]
|
[lib]
|
||||||
# the runtime needs to be a shared object -> cdylib
|
# the runtime needs to be a shared object -> cdylib
|
||||||
|
@ -51,7 +51,7 @@ where
|
|||||||
// if this fails, there is not much we can do. let's hope it failed because the process finished
|
// if this fails, there is not much we can do. let's hope it failed because the process finished
|
||||||
// in the meantime.
|
// in the meantime.
|
||||||
drop(child.kill());
|
drop(child.kill());
|
||||||
// finally, try to wait to properly clean up system ressources.
|
// finally, try to wait to properly clean up system resources.
|
||||||
drop(child.wait());
|
drop(child.wait());
|
||||||
Ok(ExitKind::Timeout)
|
Ok(ExitKind::Timeout)
|
||||||
}
|
}
|
||||||
|
@ -1,300 +1,300 @@
|
|||||||
|
//! # Concolic Tracing
|
||||||
use core::num::NonZeroUsize;
|
use core::num::NonZeroUsize;
|
||||||
|
|
||||||
#[cfg(feature = "std")]
|
#[cfg(feature = "std")]
|
||||||
use serde::{Deserialize, Serialize};
|
use serde::{Deserialize, Serialize};
|
||||||
|
|
||||||
|
/// A `SymExprRef` identifies a [`SymExpr`] in a trace. Reading a `SymExpr` from a trace will always also yield its
|
||||||
|
/// `SymExprRef`, which can be used later in the trace to identify the `SymExpr`.
|
||||||
|
/// It is also never zero, which allows for efficient use of `Option<SymExprRef>`.
|
||||||
|
///
|
||||||
|
/// In a trace, `SymExprRef`s are monotonically increasing and start at 1.
|
||||||
|
/// `SymExprRef`s are not valid across traces.
|
||||||
pub type SymExprRef = NonZeroUsize;
|
pub type SymExprRef = NonZeroUsize;
|
||||||
|
|
||||||
|
/// `SymExpr` represents a message in the serialization format.
|
||||||
|
/// The messages in the format are a perfect mirror of the methods that are called on the runtime during execution.
|
||||||
#[cfg(feature = "std")]
|
#[cfg(feature = "std")]
|
||||||
#[derive(Serialize, Deserialize, Debug)]
|
#[derive(Serialize, Deserialize, Debug, PartialEq)]
|
||||||
pub enum SymExpr {
|
pub enum SymExpr {
|
||||||
GetInputByte {
|
InputByte {
|
||||||
offset: usize,
|
offset: usize,
|
||||||
},
|
},
|
||||||
|
|
||||||
BuildInteger {
|
Integer {
|
||||||
value: u64,
|
value: u64,
|
||||||
bits: u8,
|
bits: u8,
|
||||||
},
|
},
|
||||||
BuildInteger128 {
|
Integer128 {
|
||||||
high: u64,
|
high: u64,
|
||||||
low: u64,
|
low: u64,
|
||||||
},
|
},
|
||||||
BuildFloat {
|
Float {
|
||||||
value: f64,
|
value: f64,
|
||||||
is_double: bool,
|
is_double: bool,
|
||||||
},
|
},
|
||||||
BuildNullPointer,
|
NullPointer,
|
||||||
BuildTrue,
|
True,
|
||||||
BuildFalse,
|
False,
|
||||||
BuildBool {
|
Bool {
|
||||||
value: bool,
|
value: bool,
|
||||||
},
|
},
|
||||||
|
|
||||||
BuildNeg {
|
Neg {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildAdd {
|
Add {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildSub {
|
Sub {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildMul {
|
Mul {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildUnsignedDiv {
|
UnsignedDiv {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildSignedDiv {
|
SignedDiv {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildUnsignedRem {
|
UnsignedRem {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildSignedRem {
|
SignedRem {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildShiftLeft {
|
ShiftLeft {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildLogicalShiftRight {
|
LogicalShiftRight {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildArithmeticShiftRight {
|
ArithmeticShiftRight {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
|
|
||||||
BuildSignedLessThan {
|
SignedLessThan {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildSignedLessEqual {
|
SignedLessEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildSignedGreaterThan {
|
SignedGreaterThan {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildSignedGreaterEqual {
|
SignedGreaterEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildUnsignedLessThan {
|
UnsignedLessThan {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildUnsignedLessEqual {
|
UnsignedLessEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildUnsignedGreaterThan {
|
UnsignedGreaterThan {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildUnsignedGreaterEqual {
|
UnsignedGreaterEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
|
|
||||||
BuildNot {
|
Not {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildEqual {
|
Equal {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildNotEqual {
|
NotEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
|
|
||||||
BuildBoolAnd {
|
BoolAnd {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildBoolOr {
|
BoolOr {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildBoolXor {
|
BoolXor {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
|
|
||||||
BuildAnd {
|
And {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildOr {
|
Or {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildXor {
|
Xor {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
|
|
||||||
BuildFloatOrdered {
|
FloatOrdered {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatOrderedGreaterThan {
|
FloatOrderedGreaterThan {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatOrderedGreaterEqual {
|
FloatOrderedGreaterEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatOrderedLessThan {
|
FloatOrderedLessThan {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatOrderedLessEqual {
|
FloatOrderedLessEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatOrderedEqual {
|
FloatOrderedEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatOrderedNotEqual {
|
FloatOrderedNotEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
|
|
||||||
BuildFloatUnordered {
|
FloatUnordered {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatUnorderedGreaterThan {
|
FloatUnorderedGreaterThan {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatUnorderedGreaterEqual {
|
FloatUnorderedGreaterEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatUnorderedLessThan {
|
FloatUnorderedLessThan {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatUnorderedLessEqual {
|
FloatUnorderedLessEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatUnorderedEqual {
|
FloatUnorderedEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatUnorderedNotEqual {
|
FloatUnorderedNotEqual {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
|
|
||||||
BuildFloatAbs {
|
FloatAbs {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatAdd {
|
FloatAdd {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatSub {
|
FloatSub {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatMul {
|
FloatMul {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatDiv {
|
FloatDiv {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatRem {
|
FloatRem {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
|
|
||||||
BuildSext {
|
Sext {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
bits: u8,
|
bits: u8,
|
||||||
},
|
},
|
||||||
BuildZext {
|
Zext {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
bits: u8,
|
bits: u8,
|
||||||
},
|
},
|
||||||
BuildTrunc {
|
Trunc {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
bits: u8,
|
bits: u8,
|
||||||
},
|
},
|
||||||
BuildIntToFloat {
|
IntToFloat {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
is_double: bool,
|
is_double: bool,
|
||||||
is_signed: bool,
|
is_signed: bool,
|
||||||
},
|
},
|
||||||
BuildFloatToFloat {
|
FloatToFloat {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
to_double: bool,
|
to_double: bool,
|
||||||
},
|
},
|
||||||
BuildBitsToFloat {
|
BitsToFloat {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
to_double: bool,
|
to_double: bool,
|
||||||
},
|
},
|
||||||
BuildFloatToBits {
|
FloatToBits {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
},
|
},
|
||||||
BuildFloatToSignedInteger {
|
FloatToSignedInteger {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
bits: u8,
|
bits: u8,
|
||||||
},
|
},
|
||||||
BuildFloatToUnsignedInteger {
|
FloatToUnsignedInteger {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
bits: u8,
|
bits: u8,
|
||||||
},
|
},
|
||||||
BuildBoolToBits {
|
BoolToBits {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
bits: u8,
|
bits: u8,
|
||||||
},
|
},
|
||||||
|
|
||||||
ConcatHelper {
|
Concat {
|
||||||
a: SymExprRef,
|
a: SymExprRef,
|
||||||
b: SymExprRef,
|
b: SymExprRef,
|
||||||
},
|
},
|
||||||
ExtractHelper {
|
Extract {
|
||||||
op: SymExprRef,
|
op: SymExprRef,
|
||||||
first_bit: usize,
|
first_bit: usize,
|
||||||
last_bit: usize,
|
last_bit: usize,
|
||||||
},
|
},
|
||||||
BuildExtract {
|
Insert {
|
||||||
op: SymExprRef,
|
|
||||||
offset: u64,
|
|
||||||
length: u64,
|
|
||||||
little_endian: bool,
|
|
||||||
},
|
|
||||||
BuildBswap {
|
|
||||||
op: SymExprRef,
|
|
||||||
},
|
|
||||||
BuildInsert {
|
|
||||||
target: SymExprRef,
|
target: SymExprRef,
|
||||||
to_insert: SymExprRef,
|
to_insert: SymExprRef,
|
||||||
offset: u64,
|
offset: u64,
|
||||||
little_endian: bool,
|
little_endian: bool,
|
||||||
},
|
},
|
||||||
|
|
||||||
PushPathConstraint {
|
PathConstraint {
|
||||||
constraint: SymExprRef,
|
constraint: SymExprRef,
|
||||||
taken: bool,
|
taken: bool,
|
||||||
site_id: usize,
|
site_id: usize,
|
||||||
@ -304,8 +304,6 @@ pub enum SymExpr {
|
|||||||
ExpressionsUnreachable {
|
ExpressionsUnreachable {
|
||||||
exprs: Vec<SymExprRef>,
|
exprs: Vec<SymExprRef>,
|
||||||
},
|
},
|
||||||
/// This marks the end of the trace.
|
|
||||||
End,
|
|
||||||
}
|
}
|
||||||
|
|
||||||
#[cfg(feature = "std")]
|
#[cfg(feature = "std")]
|
||||||
@ -317,10 +315,10 @@ pub const HITMAP_ENV_NAME: &str = "LIBAFL_CONCOLIC_HITMAP";
|
|||||||
/// The name of the environment variable that contains the byte offsets to be symbolized.
|
/// The name of the environment variable that contains the byte offsets to be symbolized.
|
||||||
pub const SELECTIVE_SYMBOLICATION_ENV_NAME: &str = "LIBAFL_SELECTIVE_SYMBOLICATION";
|
pub const SELECTIVE_SYMBOLICATION_ENV_NAME: &str = "LIBAFL_SELECTIVE_SYMBOLICATION";
|
||||||
|
|
||||||
/// The name of the environment variable that contains the byte offsets to be symbolized.
|
/// The name of the environment variable that signals the runtime to concretize floating point operations.
|
||||||
pub const NO_FLOAT_ENV_NAME: &str = "LIBAFL_CONCOLIC_NO_FLOAT";
|
pub const NO_FLOAT_ENV_NAME: &str = "LIBAFL_CONCOLIC_NO_FLOAT";
|
||||||
|
|
||||||
/// The name of the environment variable that contains the byte offsets to be symbolized.
|
/// The name of the environment variable that signals the runtime to perform expression pruning.
|
||||||
pub const EXPRESSION_PRUNING: &str = "LIBAFL_CONCOLIC_EXPRESSION_PRUNING";
|
pub const EXPRESSION_PRUNING: &str = "LIBAFL_CONCOLIC_EXPRESSION_PRUNING";
|
||||||
|
|
||||||
#[cfg(feature = "std")]
|
#[cfg(feature = "std")]
|
||||||
|
@ -1,17 +1,64 @@
|
|||||||
|
//! # Concolic Tracing Serialization Format
|
||||||
|
//! ## Design Goals
|
||||||
|
//! * The serialization format for concolic tracing was developed with the goal of being space and time efficient.
|
||||||
|
//! * Additionally, it should be easy to maintain and extend.
|
||||||
|
//! * It does not have to be compatible with other programming languages.
|
||||||
|
//! * It should be resilient to crashes. Since we are fuzzing, we are expecting the traced program to crash at some
|
||||||
|
//! point.
|
||||||
|
//!
|
||||||
|
//! The format as implemented fulfils these design goals.
|
||||||
|
//! Specifically:
|
||||||
|
//! * it requires only constant memory space for serialization, which allows for tracing complex and/or
|
||||||
|
//! long-running programs.
|
||||||
|
//! * the trace itself requires little space. A typical binary operation (such as an add) typically takes just 3 bytes.
|
||||||
|
//! * it easy to encode. There is no translation between the interface of the runtime itself and the trace it generates.
|
||||||
|
//! * it is similarly easy to decode and can be easily translated into an in-memory AST without overhead, because
|
||||||
|
//! expressions are decoded from leaf to root instead of root to leaf.
|
||||||
|
//! * At its core, it is just [`SymExpr`]s, which can be added to, modified and removed from with ease. The
|
||||||
|
//! definitions are automatically shared between the runtime and the consuming program, since both depend on the same
|
||||||
|
//! `LibAFL`.
|
||||||
|
//!
|
||||||
|
//! ## Techniques
|
||||||
|
//! The serialization format applies multiple techniques to achieve its goals.
|
||||||
|
//! * It uses bincode for efficient binary serialization. Crucially, bincode uses variable length integer encoding,
|
||||||
|
//! allowing it encode small integers use fewer bytes.
|
||||||
|
//! * References to previous expressions are stored relative to the current expressions id. The vast majority of
|
||||||
|
//! expressions refer to other expressions that were defined close to their use. Therefore, encoding relative references
|
||||||
|
//! keeps references small. Therefore, they make optimal use of bincodes variable length integer encoding.
|
||||||
|
//! * Ids of expressions ([`SymExprRef`]s) are implicitly derived by their position in the message stream. Effectively,
|
||||||
|
//! a counter is used to identify expressions.
|
||||||
|
//! * The current length of the trace in bytes in serialized in a fixed format at the beginning of the trace.
|
||||||
|
//! This length is updated regularly when the trace is in a consistent state. This allows the reader to avoid reading
|
||||||
|
//! malformed data if the traced process crashed.
|
||||||
|
//!
|
||||||
|
//! ## Example
|
||||||
|
//! The expression `SymExpr::BoolAnd { a: SymExpr::True, b: SymExpr::False }` would be encoded as:
|
||||||
|
//! 1. 1 byte to identify `SymExpr::True` (a)
|
||||||
|
//! 2. 1 byte to identify `SymExpr::False` (b)
|
||||||
|
//! 3. 1 byte to identify `SymExpr::BoolAnd`
|
||||||
|
//! 4. 1 byte to reference a
|
||||||
|
//! 5. 1 byte to reference b
|
||||||
|
//!
|
||||||
|
//! ... making for a total of 5 bytes.
|
||||||
|
|
||||||
#![cfg(feature = "std")]
|
#![cfg(feature = "std")]
|
||||||
|
|
||||||
use std::io::{self, Read, Seek, SeekFrom, Write};
|
use std::{
|
||||||
|
convert::TryFrom,
|
||||||
|
io::{self, Cursor, Read, Seek, SeekFrom, Write},
|
||||||
|
};
|
||||||
|
|
||||||
use bincode::{DefaultOptions, Options};
|
use bincode::{DefaultOptions, Options};
|
||||||
|
|
||||||
use super::{SymExpr, SymExprRef};
|
use super::{SymExpr, SymExprRef};
|
||||||
|
|
||||||
pub use bincode::ErrorKind;
|
pub use bincode::{ErrorKind, Result};
|
||||||
pub use bincode::Result;
|
|
||||||
|
|
||||||
fn serialization_options() -> DefaultOptions {
|
fn serialization_options() -> DefaultOptions {
|
||||||
DefaultOptions::new()
|
DefaultOptions::new()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// A `MessageFileReader` reads a stream of [`SymExpr`] and their corresponding [`SymExprRef`]s from any [`Read`].
|
||||||
pub struct MessageFileReader<R: Read> {
|
pub struct MessageFileReader<R: Read> {
|
||||||
reader: R,
|
reader: R,
|
||||||
deserializer_config: bincode::DefaultOptions,
|
deserializer_config: bincode::DefaultOptions,
|
||||||
@ -19,6 +66,7 @@ pub struct MessageFileReader<R: Read> {
|
|||||||
}
|
}
|
||||||
|
|
||||||
impl<R: Read> MessageFileReader<R> {
|
impl<R: Read> MessageFileReader<R> {
|
||||||
|
/// Construct from the given reader.
|
||||||
pub fn from_reader(reader: R) -> Self {
|
pub fn from_reader(reader: R) -> Self {
|
||||||
Self {
|
Self {
|
||||||
reader,
|
reader,
|
||||||
@ -27,15 +75,17 @@ impl<R: Read> MessageFileReader<R> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Parse the next message out of the stream.
|
||||||
|
/// [`Option::None`] is returned once the stream is depleted.
|
||||||
|
/// IO and serialization errors are passed to the caller using [`bincode::Result`].
|
||||||
|
/// Finally, the returned tuple contains the message itself as a [`SymExpr`] and the [`SymExprRef`] associated
|
||||||
|
/// with this message.
|
||||||
|
/// The `SymExprRef` may be used by following messages to refer back to this message.
|
||||||
pub fn next_message(&mut self) -> Option<bincode::Result<(SymExprRef, SymExpr)>> {
|
pub fn next_message(&mut self) -> Option<bincode::Result<(SymExprRef, SymExpr)>> {
|
||||||
match self.deserializer_config.deserialize_from(&mut self.reader) {
|
match self.deserializer_config.deserialize_from(&mut self.reader) {
|
||||||
Ok(mut message) => {
|
Ok(mut message) => {
|
||||||
if let SymExpr::End = message {
|
let message_id = self.transform_message(&mut message);
|
||||||
None
|
Some(Ok((message_id, message)))
|
||||||
} else {
|
|
||||||
let message_id = self.transform_message(&mut message);
|
|
||||||
Some(Ok((message_id, message)))
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
Err(e) => match *e {
|
Err(e) => match *e {
|
||||||
bincode::ErrorKind::Io(ref io_err) => match io_err.kind() {
|
bincode::ErrorKind::Io(ref io_err) => match io_err.kind() {
|
||||||
@ -47,89 +97,91 @@ impl<R: Read> MessageFileReader<R> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Makes the given `SymExprRef` absolute accoring to the `current_id` counter.
|
||||||
|
/// See [`MessageFileWriter::make_relative`] for the inverse function.
|
||||||
fn make_absolute(&self, expr: SymExprRef) -> SymExprRef {
|
fn make_absolute(&self, expr: SymExprRef) -> SymExprRef {
|
||||||
SymExprRef::new(self.current_id - expr.get()).unwrap()
|
SymExprRef::new(self.current_id - expr.get()).unwrap()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// This transforms the given message from it's serialized form into its in-memory form, making relative references
|
||||||
|
/// absolute and counting the `SymExprRef`s.
|
||||||
fn transform_message(&mut self, message: &mut SymExpr) -> SymExprRef {
|
fn transform_message(&mut self, message: &mut SymExpr) -> SymExprRef {
|
||||||
let ret = self.current_id;
|
let ret = self.current_id;
|
||||||
match message {
|
match message {
|
||||||
SymExpr::GetInputByte { .. }
|
SymExpr::InputByte { .. }
|
||||||
| SymExpr::BuildInteger { .. }
|
| SymExpr::Integer { .. }
|
||||||
| SymExpr::BuildInteger128 { .. }
|
| SymExpr::Integer128 { .. }
|
||||||
| SymExpr::BuildFloat { .. }
|
| SymExpr::Float { .. }
|
||||||
| SymExpr::BuildNullPointer
|
| SymExpr::NullPointer
|
||||||
| SymExpr::BuildTrue
|
| SymExpr::True
|
||||||
| SymExpr::BuildFalse
|
| SymExpr::False
|
||||||
| SymExpr::BuildBool { .. } => {
|
| SymExpr::Bool { .. } => {
|
||||||
self.current_id += 1;
|
self.current_id += 1;
|
||||||
}
|
}
|
||||||
SymExpr::BuildNeg { op }
|
SymExpr::Neg { op }
|
||||||
| SymExpr::BuildFloatAbs { op }
|
| SymExpr::FloatAbs { op }
|
||||||
| SymExpr::BuildNot { op }
|
| SymExpr::Not { op }
|
||||||
| SymExpr::BuildSext { op, .. }
|
| SymExpr::Sext { op, .. }
|
||||||
| SymExpr::BuildZext { op, .. }
|
| SymExpr::Zext { op, .. }
|
||||||
| SymExpr::BuildTrunc { op, .. }
|
| SymExpr::Trunc { op, .. }
|
||||||
| SymExpr::BuildIntToFloat { op, .. }
|
| SymExpr::IntToFloat { op, .. }
|
||||||
| SymExpr::BuildFloatToFloat { op, .. }
|
| SymExpr::FloatToFloat { op, .. }
|
||||||
| SymExpr::BuildBitsToFloat { op, .. }
|
| SymExpr::BitsToFloat { op, .. }
|
||||||
| SymExpr::BuildFloatToBits { op }
|
| SymExpr::FloatToBits { op }
|
||||||
| SymExpr::BuildFloatToSignedInteger { op, .. }
|
| SymExpr::FloatToSignedInteger { op, .. }
|
||||||
| SymExpr::BuildFloatToUnsignedInteger { op, .. }
|
| SymExpr::FloatToUnsignedInteger { op, .. }
|
||||||
| SymExpr::BuildBoolToBits { op, .. }
|
| SymExpr::BoolToBits { op, .. }
|
||||||
| SymExpr::ExtractHelper { op, .. }
|
| SymExpr::Extract { op, .. } => {
|
||||||
| SymExpr::BuildExtract { op, .. }
|
|
||||||
| SymExpr::BuildBswap { op } => {
|
|
||||||
*op = self.make_absolute(*op);
|
*op = self.make_absolute(*op);
|
||||||
self.current_id += 1;
|
self.current_id += 1;
|
||||||
}
|
}
|
||||||
SymExpr::BuildAdd { a, b }
|
SymExpr::Add { a, b }
|
||||||
| SymExpr::BuildSub { a, b }
|
| SymExpr::Sub { a, b }
|
||||||
| SymExpr::BuildMul { a, b }
|
| SymExpr::Mul { a, b }
|
||||||
| SymExpr::BuildUnsignedDiv { a, b }
|
| SymExpr::UnsignedDiv { a, b }
|
||||||
| SymExpr::BuildSignedDiv { a, b }
|
| SymExpr::SignedDiv { a, b }
|
||||||
| SymExpr::BuildUnsignedRem { a, b }
|
| SymExpr::UnsignedRem { a, b }
|
||||||
| SymExpr::BuildSignedRem { a, b }
|
| SymExpr::SignedRem { a, b }
|
||||||
| SymExpr::BuildShiftLeft { a, b }
|
| SymExpr::ShiftLeft { a, b }
|
||||||
| SymExpr::BuildLogicalShiftRight { a, b }
|
| SymExpr::LogicalShiftRight { a, b }
|
||||||
| SymExpr::BuildArithmeticShiftRight { a, b }
|
| SymExpr::ArithmeticShiftRight { a, b }
|
||||||
| SymExpr::BuildSignedLessThan { a, b }
|
| SymExpr::SignedLessThan { a, b }
|
||||||
| SymExpr::BuildSignedLessEqual { a, b }
|
| SymExpr::SignedLessEqual { a, b }
|
||||||
| SymExpr::BuildSignedGreaterThan { a, b }
|
| SymExpr::SignedGreaterThan { a, b }
|
||||||
| SymExpr::BuildSignedGreaterEqual { a, b }
|
| SymExpr::SignedGreaterEqual { a, b }
|
||||||
| SymExpr::BuildUnsignedLessThan { a, b }
|
| SymExpr::UnsignedLessThan { a, b }
|
||||||
| SymExpr::BuildUnsignedLessEqual { a, b }
|
| SymExpr::UnsignedLessEqual { a, b }
|
||||||
| SymExpr::BuildUnsignedGreaterThan { a, b }
|
| SymExpr::UnsignedGreaterThan { a, b }
|
||||||
| SymExpr::BuildUnsignedGreaterEqual { a, b }
|
| SymExpr::UnsignedGreaterEqual { a, b }
|
||||||
| SymExpr::BuildEqual { a, b }
|
| SymExpr::Equal { a, b }
|
||||||
| SymExpr::BuildNotEqual { a, b }
|
| SymExpr::NotEqual { a, b }
|
||||||
| SymExpr::BuildBoolAnd { a, b }
|
| SymExpr::BoolAnd { a, b }
|
||||||
| SymExpr::BuildBoolOr { a, b }
|
| SymExpr::BoolOr { a, b }
|
||||||
| SymExpr::BuildBoolXor { a, b }
|
| SymExpr::BoolXor { a, b }
|
||||||
| SymExpr::BuildAnd { a, b }
|
| SymExpr::And { a, b }
|
||||||
| SymExpr::BuildOr { a, b }
|
| SymExpr::Or { a, b }
|
||||||
| SymExpr::BuildXor { a, b }
|
| SymExpr::Xor { a, b }
|
||||||
| SymExpr::BuildFloatOrdered { a, b }
|
| SymExpr::FloatOrdered { a, b }
|
||||||
| SymExpr::BuildFloatOrderedGreaterThan { a, b }
|
| SymExpr::FloatOrderedGreaterThan { a, b }
|
||||||
| SymExpr::BuildFloatOrderedGreaterEqual { a, b }
|
| SymExpr::FloatOrderedGreaterEqual { a, b }
|
||||||
| SymExpr::BuildFloatOrderedLessThan { a, b }
|
| SymExpr::FloatOrderedLessThan { a, b }
|
||||||
| SymExpr::BuildFloatOrderedLessEqual { a, b }
|
| SymExpr::FloatOrderedLessEqual { a, b }
|
||||||
| SymExpr::BuildFloatOrderedEqual { a, b }
|
| SymExpr::FloatOrderedEqual { a, b }
|
||||||
| SymExpr::BuildFloatOrderedNotEqual { a, b }
|
| SymExpr::FloatOrderedNotEqual { a, b }
|
||||||
| SymExpr::BuildFloatUnordered { a, b }
|
| SymExpr::FloatUnordered { a, b }
|
||||||
| SymExpr::BuildFloatUnorderedGreaterThan { a, b }
|
| SymExpr::FloatUnorderedGreaterThan { a, b }
|
||||||
| SymExpr::BuildFloatUnorderedGreaterEqual { a, b }
|
| SymExpr::FloatUnorderedGreaterEqual { a, b }
|
||||||
| SymExpr::BuildFloatUnorderedLessThan { a, b }
|
| SymExpr::FloatUnorderedLessThan { a, b }
|
||||||
| SymExpr::BuildFloatUnorderedLessEqual { a, b }
|
| SymExpr::FloatUnorderedLessEqual { a, b }
|
||||||
| SymExpr::BuildFloatUnorderedEqual { a, b }
|
| SymExpr::FloatUnorderedEqual { a, b }
|
||||||
| SymExpr::BuildFloatUnorderedNotEqual { a, b }
|
| SymExpr::FloatUnorderedNotEqual { a, b }
|
||||||
| SymExpr::BuildFloatAdd { a, b }
|
| SymExpr::FloatAdd { a, b }
|
||||||
| SymExpr::BuildFloatSub { a, b }
|
| SymExpr::FloatSub { a, b }
|
||||||
| SymExpr::BuildFloatMul { a, b }
|
| SymExpr::FloatMul { a, b }
|
||||||
| SymExpr::BuildFloatDiv { a, b }
|
| SymExpr::FloatDiv { a, b }
|
||||||
| SymExpr::BuildFloatRem { a, b }
|
| SymExpr::FloatRem { a, b }
|
||||||
| SymExpr::ConcatHelper { a, b }
|
| SymExpr::Concat { a, b }
|
||||||
| SymExpr::BuildInsert {
|
| SymExpr::Insert {
|
||||||
target: a,
|
target: a,
|
||||||
to_insert: b,
|
to_insert: b,
|
||||||
..
|
..
|
||||||
@ -138,7 +190,7 @@ impl<R: Read> MessageFileReader<R> {
|
|||||||
*b = self.make_absolute(*b);
|
*b = self.make_absolute(*b);
|
||||||
self.current_id += 1;
|
self.current_id += 1;
|
||||||
}
|
}
|
||||||
SymExpr::PushPathConstraint { constraint: op, .. } => {
|
SymExpr::PathConstraint { constraint: op, .. } => {
|
||||||
*op = self.make_absolute(*op);
|
*op = self.make_absolute(*op);
|
||||||
}
|
}
|
||||||
SymExpr::ExpressionsUnreachable { exprs } => {
|
SymExpr::ExpressionsUnreachable { exprs } => {
|
||||||
@ -146,14 +198,13 @@ impl<R: Read> MessageFileReader<R> {
|
|||||||
*expr = self.make_absolute(*expr);
|
*expr = self.make_absolute(*expr);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
SymExpr::End => {
|
|
||||||
panic!("should not pass End message to this function");
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
SymExprRef::new(ret).unwrap()
|
SymExprRef::new(ret).unwrap()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// A `MessageFileWriter` writes a stream of [`SymExpr`] to any [`Write`]. For each written expression, it returns
|
||||||
|
/// a [`SymExprRef`] which should be used to refer back to it.
|
||||||
pub struct MessageFileWriter<W: Write> {
|
pub struct MessageFileWriter<W: Write> {
|
||||||
id_counter: usize,
|
id_counter: usize,
|
||||||
writer: W,
|
writer: W,
|
||||||
@ -162,6 +213,7 @@ pub struct MessageFileWriter<W: Write> {
|
|||||||
}
|
}
|
||||||
|
|
||||||
impl<W: Write + Seek> MessageFileWriter<W> {
|
impl<W: Write + Seek> MessageFileWriter<W> {
|
||||||
|
/// Create a `MessageFileWriter` from the given [`Write`].
|
||||||
pub fn from_writer(mut writer: W) -> io::Result<Self> {
|
pub fn from_writer(mut writer: W) -> io::Result<Self> {
|
||||||
let writer_start_position = writer.stream_position()?;
|
let writer_start_position = writer.stream_position()?;
|
||||||
// write dummy trace length
|
// write dummy trace length
|
||||||
@ -190,7 +242,8 @@ impl<W: Write + Seek> MessageFileWriter<W> {
|
|||||||
Ok(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn end(&mut self) -> io::Result<()> {
|
/// Updates the trace header which stores the total length of the trace in bytes.
|
||||||
|
pub fn update_trace_header(&mut self) -> io::Result<()> {
|
||||||
self.write_trace_size()?;
|
self.write_trace_size()?;
|
||||||
Ok(())
|
Ok(())
|
||||||
}
|
}
|
||||||
@ -199,86 +252,86 @@ impl<W: Write + Seek> MessageFileWriter<W> {
|
|||||||
SymExprRef::new(self.id_counter - expr.get()).unwrap()
|
SymExprRef::new(self.id_counter - expr.get()).unwrap()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Writes a message to the stream and returns the [`SymExprRef`] that should be used to refer back to this message.
|
||||||
|
/// May error when the underlying `Write` errors or when there is a serialization error.
|
||||||
#[allow(clippy::too_many_lines)]
|
#[allow(clippy::too_many_lines)]
|
||||||
pub fn write_message(&mut self, mut message: SymExpr) -> bincode::Result<SymExprRef> {
|
pub fn write_message(&mut self, mut message: SymExpr) -> bincode::Result<SymExprRef> {
|
||||||
let current_id = self.id_counter;
|
let current_id = self.id_counter;
|
||||||
match &mut message {
|
match &mut message {
|
||||||
SymExpr::GetInputByte { .. }
|
SymExpr::InputByte { .. }
|
||||||
| SymExpr::BuildInteger { .. }
|
| SymExpr::Integer { .. }
|
||||||
| SymExpr::BuildInteger128 { .. }
|
| SymExpr::Integer128 { .. }
|
||||||
| SymExpr::BuildFloat { .. }
|
| SymExpr::Float { .. }
|
||||||
| SymExpr::BuildNullPointer
|
| SymExpr::NullPointer
|
||||||
| SymExpr::BuildTrue
|
| SymExpr::True
|
||||||
| SymExpr::BuildFalse
|
| SymExpr::False
|
||||||
| SymExpr::BuildBool { .. } => {
|
| SymExpr::Bool { .. } => {
|
||||||
self.id_counter += 1;
|
self.id_counter += 1;
|
||||||
}
|
}
|
||||||
SymExpr::BuildNeg { op }
|
SymExpr::Neg { op }
|
||||||
| SymExpr::BuildFloatAbs { op }
|
| SymExpr::FloatAbs { op }
|
||||||
| SymExpr::BuildNot { op }
|
| SymExpr::Not { op }
|
||||||
| SymExpr::BuildSext { op, .. }
|
| SymExpr::Sext { op, .. }
|
||||||
| SymExpr::BuildZext { op, .. }
|
| SymExpr::Zext { op, .. }
|
||||||
| SymExpr::BuildTrunc { op, .. }
|
| SymExpr::Trunc { op, .. }
|
||||||
| SymExpr::BuildIntToFloat { op, .. }
|
| SymExpr::IntToFloat { op, .. }
|
||||||
| SymExpr::BuildFloatToFloat { op, .. }
|
| SymExpr::FloatToFloat { op, .. }
|
||||||
| SymExpr::BuildBitsToFloat { op, .. }
|
| SymExpr::BitsToFloat { op, .. }
|
||||||
| SymExpr::BuildFloatToBits { op }
|
| SymExpr::FloatToBits { op }
|
||||||
| SymExpr::BuildFloatToSignedInteger { op, .. }
|
| SymExpr::FloatToSignedInteger { op, .. }
|
||||||
| SymExpr::BuildFloatToUnsignedInteger { op, .. }
|
| SymExpr::FloatToUnsignedInteger { op, .. }
|
||||||
| SymExpr::BuildBoolToBits { op, .. }
|
| SymExpr::BoolToBits { op, .. }
|
||||||
| SymExpr::ExtractHelper { op, .. }
|
| SymExpr::Extract { op, .. } => {
|
||||||
| SymExpr::BuildExtract { op, .. }
|
|
||||||
| SymExpr::BuildBswap { op } => {
|
|
||||||
*op = self.make_relative(*op);
|
*op = self.make_relative(*op);
|
||||||
self.id_counter += 1;
|
self.id_counter += 1;
|
||||||
}
|
}
|
||||||
SymExpr::BuildAdd { a, b }
|
SymExpr::Add { a, b }
|
||||||
| SymExpr::BuildSub { a, b }
|
| SymExpr::Sub { a, b }
|
||||||
| SymExpr::BuildMul { a, b }
|
| SymExpr::Mul { a, b }
|
||||||
| SymExpr::BuildUnsignedDiv { a, b }
|
| SymExpr::UnsignedDiv { a, b }
|
||||||
| SymExpr::BuildSignedDiv { a, b }
|
| SymExpr::SignedDiv { a, b }
|
||||||
| SymExpr::BuildUnsignedRem { a, b }
|
| SymExpr::UnsignedRem { a, b }
|
||||||
| SymExpr::BuildSignedRem { a, b }
|
| SymExpr::SignedRem { a, b }
|
||||||
| SymExpr::BuildShiftLeft { a, b }
|
| SymExpr::ShiftLeft { a, b }
|
||||||
| SymExpr::BuildLogicalShiftRight { a, b }
|
| SymExpr::LogicalShiftRight { a, b }
|
||||||
| SymExpr::BuildArithmeticShiftRight { a, b }
|
| SymExpr::ArithmeticShiftRight { a, b }
|
||||||
| SymExpr::BuildSignedLessThan { a, b }
|
| SymExpr::SignedLessThan { a, b }
|
||||||
| SymExpr::BuildSignedLessEqual { a, b }
|
| SymExpr::SignedLessEqual { a, b }
|
||||||
| SymExpr::BuildSignedGreaterThan { a, b }
|
| SymExpr::SignedGreaterThan { a, b }
|
||||||
| SymExpr::BuildSignedGreaterEqual { a, b }
|
| SymExpr::SignedGreaterEqual { a, b }
|
||||||
| SymExpr::BuildUnsignedLessThan { a, b }
|
| SymExpr::UnsignedLessThan { a, b }
|
||||||
| SymExpr::BuildUnsignedLessEqual { a, b }
|
| SymExpr::UnsignedLessEqual { a, b }
|
||||||
| SymExpr::BuildUnsignedGreaterThan { a, b }
|
| SymExpr::UnsignedGreaterThan { a, b }
|
||||||
| SymExpr::BuildUnsignedGreaterEqual { a, b }
|
| SymExpr::UnsignedGreaterEqual { a, b }
|
||||||
| SymExpr::BuildEqual { a, b }
|
| SymExpr::Equal { a, b }
|
||||||
| SymExpr::BuildNotEqual { a, b }
|
| SymExpr::NotEqual { a, b }
|
||||||
| SymExpr::BuildBoolAnd { a, b }
|
| SymExpr::BoolAnd { a, b }
|
||||||
| SymExpr::BuildBoolOr { a, b }
|
| SymExpr::BoolOr { a, b }
|
||||||
| SymExpr::BuildBoolXor { a, b }
|
| SymExpr::BoolXor { a, b }
|
||||||
| SymExpr::BuildAnd { a, b }
|
| SymExpr::And { a, b }
|
||||||
| SymExpr::BuildOr { a, b }
|
| SymExpr::Or { a, b }
|
||||||
| SymExpr::BuildXor { a, b }
|
| SymExpr::Xor { a, b }
|
||||||
| SymExpr::BuildFloatOrdered { a, b }
|
| SymExpr::FloatOrdered { a, b }
|
||||||
| SymExpr::BuildFloatOrderedGreaterThan { a, b }
|
| SymExpr::FloatOrderedGreaterThan { a, b }
|
||||||
| SymExpr::BuildFloatOrderedGreaterEqual { a, b }
|
| SymExpr::FloatOrderedGreaterEqual { a, b }
|
||||||
| SymExpr::BuildFloatOrderedLessThan { a, b }
|
| SymExpr::FloatOrderedLessThan { a, b }
|
||||||
| SymExpr::BuildFloatOrderedLessEqual { a, b }
|
| SymExpr::FloatOrderedLessEqual { a, b }
|
||||||
| SymExpr::BuildFloatOrderedEqual { a, b }
|
| SymExpr::FloatOrderedEqual { a, b }
|
||||||
| SymExpr::BuildFloatOrderedNotEqual { a, b }
|
| SymExpr::FloatOrderedNotEqual { a, b }
|
||||||
| SymExpr::BuildFloatUnordered { a, b }
|
| SymExpr::FloatUnordered { a, b }
|
||||||
| SymExpr::BuildFloatUnorderedGreaterThan { a, b }
|
| SymExpr::FloatUnorderedGreaterThan { a, b }
|
||||||
| SymExpr::BuildFloatUnorderedGreaterEqual { a, b }
|
| SymExpr::FloatUnorderedGreaterEqual { a, b }
|
||||||
| SymExpr::BuildFloatUnorderedLessThan { a, b }
|
| SymExpr::FloatUnorderedLessThan { a, b }
|
||||||
| SymExpr::BuildFloatUnorderedLessEqual { a, b }
|
| SymExpr::FloatUnorderedLessEqual { a, b }
|
||||||
| SymExpr::BuildFloatUnorderedEqual { a, b }
|
| SymExpr::FloatUnorderedEqual { a, b }
|
||||||
| SymExpr::BuildFloatUnorderedNotEqual { a, b }
|
| SymExpr::FloatUnorderedNotEqual { a, b }
|
||||||
| SymExpr::BuildFloatAdd { a, b }
|
| SymExpr::FloatAdd { a, b }
|
||||||
| SymExpr::BuildFloatSub { a, b }
|
| SymExpr::FloatSub { a, b }
|
||||||
| SymExpr::BuildFloatMul { a, b }
|
| SymExpr::FloatMul { a, b }
|
||||||
| SymExpr::BuildFloatDiv { a, b }
|
| SymExpr::FloatDiv { a, b }
|
||||||
| SymExpr::BuildFloatRem { a, b }
|
| SymExpr::FloatRem { a, b }
|
||||||
| SymExpr::ConcatHelper { a, b }
|
| SymExpr::Concat { a, b }
|
||||||
| SymExpr::BuildInsert {
|
| SymExpr::Insert {
|
||||||
target: a,
|
target: a,
|
||||||
to_insert: b,
|
to_insert: b,
|
||||||
..
|
..
|
||||||
@ -287,7 +340,7 @@ impl<W: Write + Seek> MessageFileWriter<W> {
|
|||||||
*b = self.make_relative(*b);
|
*b = self.make_relative(*b);
|
||||||
self.id_counter += 1;
|
self.id_counter += 1;
|
||||||
}
|
}
|
||||||
SymExpr::PushPathConstraint { constraint: op, .. } => {
|
SymExpr::PathConstraint { constraint: op, .. } => {
|
||||||
*op = self.make_relative(*op);
|
*op = self.make_relative(*op);
|
||||||
}
|
}
|
||||||
SymExpr::ExpressionsUnreachable { exprs } => {
|
SymExpr::ExpressionsUnreachable { exprs } => {
|
||||||
@ -295,74 +348,142 @@ impl<W: Write + Seek> MessageFileWriter<W> {
|
|||||||
*expr = self.make_relative(*expr);
|
*expr = self.make_relative(*expr);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
SymExpr::End => {}
|
|
||||||
}
|
}
|
||||||
self.serialization_options
|
self.serialization_options
|
||||||
.serialize_into(&mut self.writer, &message)?;
|
.serialize_into(&mut self.writer, &message)?;
|
||||||
// for every path constraint, make sure we can later decode it in case we crash by updating the trace header
|
// for every path constraint, make sure we can later decode it in case we crash by updating the trace header
|
||||||
if let SymExpr::PushPathConstraint { .. } = &message {
|
if let SymExpr::PathConstraint { .. } = &message {
|
||||||
self.write_trace_size()?;
|
self.write_trace_size()?;
|
||||||
}
|
}
|
||||||
Ok(SymExprRef::new(current_id).unwrap())
|
Ok(SymExprRef::new(current_id).unwrap())
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub mod shared_memory {
|
#[cfg(test)]
|
||||||
use std::{
|
mod serialization_tests {
|
||||||
convert::TryFrom,
|
use std::io::Cursor;
|
||||||
io::{self, Cursor, Read},
|
|
||||||
};
|
|
||||||
|
|
||||||
use crate::bolts::shmem::{ShMem, ShMemCursor, ShMemProvider, StdShMemProvider};
|
use super::{MessageFileReader, MessageFileWriter, SymExpr};
|
||||||
|
|
||||||
use super::{MessageFileReader, MessageFileWriter};
|
/// This test intends to ensure that the serialization format can efficiently encode the required information.
|
||||||
|
/// This is mainly useful to fail if any changes should be made in the future that (inadvertently) reduce
|
||||||
pub const DEFAULT_ENV_NAME: &str = "SHARED_MEMORY_MESSAGES";
|
/// serialization efficiency.
|
||||||
pub const DEFAULT_SIZE: usize = 1024 * 1024 * 1024;
|
#[test]
|
||||||
|
fn efficient_serialization() {
|
||||||
impl<'buffer> MessageFileReader<Cursor<&'buffer [u8]>> {
|
let mut buf = Vec::new();
|
||||||
#[must_use]
|
{
|
||||||
pub fn from_buffer(buffer: &'buffer [u8]) -> Self {
|
let mut cursor = Cursor::new(&mut buf);
|
||||||
Self::from_reader(Cursor::new(buffer))
|
let mut writer = MessageFileWriter::from_writer(&mut cursor).unwrap();
|
||||||
}
|
let a = writer.write_message(SymExpr::True).unwrap();
|
||||||
|
let b = writer.write_message(SymExpr::True).unwrap();
|
||||||
pub fn from_length_prefixed_buffer(mut buffer: &'buffer [u8]) -> io::Result<Self> {
|
writer.write_message(SymExpr::And { a, b }).unwrap();
|
||||||
let mut len_buf = 0u64.to_le_bytes();
|
writer.update_trace_header().unwrap();
|
||||||
buffer.read_exact(&mut len_buf)?;
|
|
||||||
let buffer_len = u64::from_le_bytes(len_buf);
|
|
||||||
assert!(usize::try_from(buffer_len).is_ok());
|
|
||||||
let buffer_len = buffer_len as usize;
|
|
||||||
let (buffer, _) = buffer.split_at(buffer_len);
|
|
||||||
Ok(Self::from_buffer(buffer))
|
|
||||||
}
|
|
||||||
|
|
||||||
#[must_use]
|
|
||||||
pub fn get_buffer(&self) -> &[u8] {
|
|
||||||
self.reader.get_ref()
|
|
||||||
}
|
}
|
||||||
|
let expected_size = 8 + // the header takes 8 bytes to encode the length of the trace
|
||||||
|
1 + // tag to create SymExpr::True (a)
|
||||||
|
1 + // tag to create SymExpr::True (b)
|
||||||
|
1 + // tag to create SymExpr::And
|
||||||
|
1 + // reference to a
|
||||||
|
1; // reference to b
|
||||||
|
assert_eq!(buf.len(), expected_size);
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<T: ShMem> MessageFileWriter<ShMemCursor<T>> {
|
/// This test intends to verify that a trace written by [`MessageFileWriter`] can indeed be read back by
|
||||||
pub fn from_shmem(shmem: T) -> io::Result<Self> {
|
/// [`MessageFileReader`].
|
||||||
Self::from_writer(ShMemCursor::new(shmem))
|
#[test]
|
||||||
|
fn serialization_roundtrip() {
|
||||||
|
let mut buf = Vec::new();
|
||||||
|
{
|
||||||
|
let mut cursor = Cursor::new(&mut buf);
|
||||||
|
let mut writer = MessageFileWriter::from_writer(&mut cursor).unwrap();
|
||||||
|
let a = writer.write_message(SymExpr::True).unwrap();
|
||||||
|
let b = writer.write_message(SymExpr::True).unwrap();
|
||||||
|
writer.write_message(SymExpr::And { a, b }).unwrap();
|
||||||
|
writer.update_trace_header().unwrap();
|
||||||
}
|
}
|
||||||
|
let mut reader = MessageFileReader::from_length_prefixed_buffer(&buf).unwrap();
|
||||||
|
let (first_bool_id, first_bool) = reader.next_message().unwrap().unwrap();
|
||||||
|
assert_eq!(first_bool, SymExpr::True);
|
||||||
|
let (second_bool_id, second_bool) = reader.next_message().unwrap().unwrap();
|
||||||
|
assert_eq!(second_bool, SymExpr::True);
|
||||||
|
let (_, and) = reader.next_message().unwrap().unwrap();
|
||||||
|
assert_eq!(
|
||||||
|
and,
|
||||||
|
SymExpr::And {
|
||||||
|
a: first_bool_id,
|
||||||
|
b: second_bool_id
|
||||||
|
}
|
||||||
|
);
|
||||||
|
assert!(reader.next_message().is_none());
|
||||||
}
|
}
|
||||||
|
|
||||||
impl MessageFileWriter<ShMemCursor<<StdShMemProvider as ShMemProvider>::Mem>> {
|
|
||||||
pub fn from_stdshmem_env_with_name(env_name: impl AsRef<str>) -> io::Result<Self> {
|
|
||||||
Self::from_shmem(
|
|
||||||
StdShMemProvider::new()
|
|
||||||
.expect("unable to initialize StdShMemProvider")
|
|
||||||
.existing_from_env(env_name.as_ref())
|
|
||||||
.expect("unable to get shared memory from env"),
|
|
||||||
)
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn from_stdshmem_default_env() -> io::Result<Self> {
|
|
||||||
Self::from_stdshmem_env_with_name(DEFAULT_ENV_NAME)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub type StdShMemMessageFileWriter =
|
|
||||||
MessageFileWriter<ShMemCursor<<StdShMemProvider as ShMemProvider>::Mem>>;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
use crate::bolts::shmem::{ShMem, ShMemCursor, ShMemProvider, StdShMemProvider};
|
||||||
|
|
||||||
|
/// The default environment variable name to use for the shared memory used by the concolic tracing
|
||||||
|
pub const DEFAULT_ENV_NAME: &str = "SHARED_MEMORY_MESSAGES";
|
||||||
|
|
||||||
|
/// The default shared memory size used by the concolic tracing.
|
||||||
|
///
|
||||||
|
/// This amounts to 1GiB of memory, which is considered to be enough for any reasonable trace. It is also assumed
|
||||||
|
/// that the memory will not be phsyically mapped until accessed, alleviating reource concerns.
|
||||||
|
pub const DEFAULT_SIZE: usize = 1024 * 1024 * 1024;
|
||||||
|
|
||||||
|
impl<'buffer> MessageFileReader<Cursor<&'buffer [u8]>> {
|
||||||
|
/// Creates a new `MessageFileReader` from the given buffer.
|
||||||
|
/// It is expected that trace in this buffer is not length prefixed and the buffer itself should have the exact
|
||||||
|
/// length of the trace (ie. contain no partial message).
|
||||||
|
/// See also [`MessageFileReader::from_length_prefixed_buffer`].
|
||||||
|
#[must_use]
|
||||||
|
pub fn from_buffer(buffer: &'buffer [u8]) -> Self {
|
||||||
|
Self::from_reader(Cursor::new(buffer))
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Creates a new `MessageFileReader` from the given buffer, expecting the contained trace to be prefixed by the
|
||||||
|
/// trace length (as generated by the [`MessageFileWriter`]).
|
||||||
|
/// See also [`MessageFileReader::from_buffer`].
|
||||||
|
pub fn from_length_prefixed_buffer(mut buffer: &'buffer [u8]) -> io::Result<Self> {
|
||||||
|
let mut len_buf = 0u64.to_le_bytes();
|
||||||
|
buffer.read_exact(&mut len_buf)?;
|
||||||
|
let buffer_len = u64::from_le_bytes(len_buf);
|
||||||
|
assert!(usize::try_from(buffer_len).is_ok());
|
||||||
|
let buffer_len = buffer_len as usize;
|
||||||
|
let (buffer, _) = buffer.split_at(buffer_len);
|
||||||
|
Ok(Self::from_buffer(buffer))
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Gets the currently used buffer. If the buffer was length prefixed, the returned buffer does not contain the
|
||||||
|
/// prefix and is exactly as many bytes long as the prefix specified. Effectively, the length prefix is removed and
|
||||||
|
/// used to limit the buffer.
|
||||||
|
#[must_use]
|
||||||
|
pub fn get_buffer(&self) -> &[u8] {
|
||||||
|
self.reader.get_ref()
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<T: ShMem> MessageFileWriter<ShMemCursor<T>> {
|
||||||
|
/// Creates a new `MessageFileWriter` from the given [`ShMemCursor`].
|
||||||
|
pub fn from_shmem(shmem: T) -> io::Result<Self> {
|
||||||
|
Self::from_writer(ShMemCursor::new(shmem))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl MessageFileWriter<ShMemCursor<<StdShMemProvider as ShMemProvider>::Mem>> {
|
||||||
|
/// Creates a new `MessageFileWriter` by reading a [`StdShMem`] from the given environment variable.
|
||||||
|
pub fn from_stdshmem_env_with_name(env_name: impl AsRef<str>) -> io::Result<Self> {
|
||||||
|
Self::from_shmem(
|
||||||
|
StdShMemProvider::new()
|
||||||
|
.expect("unable to initialize StdShMemProvider")
|
||||||
|
.existing_from_env(env_name.as_ref())
|
||||||
|
.expect("unable to get shared memory from env"),
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Creates a new `MessageFileWriter` by reading a [`StdShMem`] using [`DEFAULT_ENV_NAME`].
|
||||||
|
pub fn from_stdshmem_default_env() -> io::Result<Self> {
|
||||||
|
Self::from_stdshmem_env_with_name(DEFAULT_ENV_NAME)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub type StdShMemMessageFileWriter =
|
||||||
|
MessageFileWriter<ShMemCursor<<StdShMemProvider as ShMemProvider>::Mem>>;
|
||||||
|
@ -159,39 +159,39 @@ fn generate_mutations(iter: impl Iterator<Item = (SymExprRef, SymExpr)>) -> Vec<
|
|||||||
|
|
||||||
for (id, msg) in iter {
|
for (id, msg) in iter {
|
||||||
let z3_expr: Option<Dynamic> = match msg {
|
let z3_expr: Option<Dynamic> = match msg {
|
||||||
SymExpr::GetInputByte { offset } => {
|
SymExpr::InputByte { offset } => {
|
||||||
Some(BV::new_const(&ctx, Symbol::Int(offset as u32), 8).into())
|
Some(BV::new_const(&ctx, Symbol::Int(offset as u32), 8).into())
|
||||||
}
|
}
|
||||||
SymExpr::BuildInteger { value, bits } => {
|
SymExpr::Integer { value, bits } => {
|
||||||
Some(BV::from_u64(&ctx, value, u32::from(bits)).into())
|
Some(BV::from_u64(&ctx, value, u32::from(bits)).into())
|
||||||
}
|
}
|
||||||
SymExpr::BuildInteger128 { high: _, low: _ } => todo!(),
|
SymExpr::Integer128 { high: _, low: _ } => todo!(),
|
||||||
SymExpr::BuildNullPointer => {
|
SymExpr::NullPointer => {
|
||||||
Some(BV::from_u64(&ctx, 0, (8 * size_of::<usize>()) as u32).into())
|
Some(BV::from_u64(&ctx, 0, (8 * size_of::<usize>()) as u32).into())
|
||||||
}
|
}
|
||||||
SymExpr::BuildTrue => Some(Bool::from_bool(&ctx, true).into()),
|
SymExpr::True => Some(Bool::from_bool(&ctx, true).into()),
|
||||||
SymExpr::BuildFalse => Some(Bool::from_bool(&ctx, false).into()),
|
SymExpr::False => Some(Bool::from_bool(&ctx, false).into()),
|
||||||
SymExpr::BuildBool { value } => Some(Bool::from_bool(&ctx, value).into()),
|
SymExpr::Bool { value } => Some(Bool::from_bool(&ctx, value).into()),
|
||||||
SymExpr::BuildNeg { op } => Some(bv!(op).bvneg().into()),
|
SymExpr::Neg { op } => Some(bv!(op).bvneg().into()),
|
||||||
SymExpr::BuildAdd { a, b } => bv_binop!(a bvadd b),
|
SymExpr::Add { a, b } => bv_binop!(a bvadd b),
|
||||||
SymExpr::BuildSub { a, b } => bv_binop!(a bvsub b),
|
SymExpr::Sub { a, b } => bv_binop!(a bvsub b),
|
||||||
SymExpr::BuildMul { a, b } => bv_binop!(a bvmul b),
|
SymExpr::Mul { a, b } => bv_binop!(a bvmul b),
|
||||||
SymExpr::BuildUnsignedDiv { a, b } => bv_binop!(a bvudiv b),
|
SymExpr::UnsignedDiv { a, b } => bv_binop!(a bvudiv b),
|
||||||
SymExpr::BuildSignedDiv { a, b } => bv_binop!(a bvsdiv b),
|
SymExpr::SignedDiv { a, b } => bv_binop!(a bvsdiv b),
|
||||||
SymExpr::BuildUnsignedRem { a, b } => bv_binop!(a bvurem b),
|
SymExpr::UnsignedRem { a, b } => bv_binop!(a bvurem b),
|
||||||
SymExpr::BuildSignedRem { a, b } => bv_binop!(a bvsrem b),
|
SymExpr::SignedRem { a, b } => bv_binop!(a bvsrem b),
|
||||||
SymExpr::BuildShiftLeft { a, b } => bv_binop!(a bvshl b),
|
SymExpr::ShiftLeft { a, b } => bv_binop!(a bvshl b),
|
||||||
SymExpr::BuildLogicalShiftRight { a, b } => bv_binop!(a bvlshr b),
|
SymExpr::LogicalShiftRight { a, b } => bv_binop!(a bvlshr b),
|
||||||
SymExpr::BuildArithmeticShiftRight { a, b } => bv_binop!(a bvashr b),
|
SymExpr::ArithmeticShiftRight { a, b } => bv_binop!(a bvashr b),
|
||||||
SymExpr::BuildSignedLessThan { a, b } => bv_binop!(a bvslt b),
|
SymExpr::SignedLessThan { a, b } => bv_binop!(a bvslt b),
|
||||||
SymExpr::BuildSignedLessEqual { a, b } => bv_binop!(a bvsle b),
|
SymExpr::SignedLessEqual { a, b } => bv_binop!(a bvsle b),
|
||||||
SymExpr::BuildSignedGreaterThan { a, b } => bv_binop!(a bvsgt b),
|
SymExpr::SignedGreaterThan { a, b } => bv_binop!(a bvsgt b),
|
||||||
SymExpr::BuildSignedGreaterEqual { a, b } => bv_binop!(a bvsge b),
|
SymExpr::SignedGreaterEqual { a, b } => bv_binop!(a bvsge b),
|
||||||
SymExpr::BuildUnsignedLessThan { a, b } => bv_binop!(a bvult b),
|
SymExpr::UnsignedLessThan { a, b } => bv_binop!(a bvult b),
|
||||||
SymExpr::BuildUnsignedLessEqual { a, b } => bv_binop!(a bvule b),
|
SymExpr::UnsignedLessEqual { a, b } => bv_binop!(a bvule b),
|
||||||
SymExpr::BuildUnsignedGreaterThan { a, b } => bv_binop!(a bvugt b),
|
SymExpr::UnsignedGreaterThan { a, b } => bv_binop!(a bvugt b),
|
||||||
SymExpr::BuildUnsignedGreaterEqual { a, b } => bv_binop!(a bvuge b),
|
SymExpr::UnsignedGreaterEqual { a, b } => bv_binop!(a bvuge b),
|
||||||
SymExpr::BuildNot { op } => {
|
SymExpr::Not { op } => {
|
||||||
let translated = &translation[&op];
|
let translated = &translation[&op];
|
||||||
Some(if let Some(bv) = translated.as_bv() {
|
Some(if let Some(bv) = translated.as_bv() {
|
||||||
bv.bvnot().into()
|
bv.bvnot().into()
|
||||||
@ -204,22 +204,18 @@ fn generate_mutations(iter: impl Iterator<Item = (SymExprRef, SymExpr)>) -> Vec<
|
|||||||
)
|
)
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
SymExpr::BuildEqual { a, b } => Some(translation[&a]._eq(&translation[&b]).into()),
|
SymExpr::Equal { a, b } => Some(translation[&a]._eq(&translation[&b]).into()),
|
||||||
SymExpr::BuildNotEqual { a, b } => {
|
SymExpr::NotEqual { a, b } => Some(translation[&a]._eq(&translation[&b]).not().into()),
|
||||||
Some(translation[&a]._eq(&translation[&b]).not().into())
|
SymExpr::BoolAnd { a, b } => Some(Bool::and(&ctx, &[&bool!(a), &bool!(b)]).into()),
|
||||||
}
|
SymExpr::BoolOr { a, b } => Some(Bool::or(&ctx, &[&bool!(a), &bool!(b)]).into()),
|
||||||
SymExpr::BuildBoolAnd { a, b } => Some(Bool::and(&ctx, &[&bool!(a), &bool!(b)]).into()),
|
SymExpr::BoolXor { a, b } => Some(bool!(a).xor(&bool!(b)).into()),
|
||||||
SymExpr::BuildBoolOr { a, b } => Some(Bool::or(&ctx, &[&bool!(a), &bool!(b)]).into()),
|
SymExpr::And { a, b } => bv_binop!(a bvand b),
|
||||||
SymExpr::BuildBoolXor { a, b } => Some(bool!(a).xor(&bool!(b)).into()),
|
SymExpr::Or { a, b } => bv_binop!(a bvor b),
|
||||||
SymExpr::BuildAnd { a, b } => bv_binop!(a bvand b),
|
SymExpr::Xor { a, b } => bv_binop!(a bvxor b),
|
||||||
SymExpr::BuildOr { a, b } => bv_binop!(a bvor b),
|
SymExpr::Sext { op, bits } => Some(bv!(op).sign_ext(u32::from(bits)).into()),
|
||||||
SymExpr::BuildXor { a, b } => bv_binop!(a bvxor b),
|
SymExpr::Zext { op, bits } => Some(bv!(op).zero_ext(u32::from(bits)).into()),
|
||||||
SymExpr::BuildSext { op, bits } => Some(bv!(op).sign_ext(u32::from(bits)).into()),
|
SymExpr::Trunc { op, bits } => Some(bv!(op).extract(u32::from(bits - 1), 0).into()),
|
||||||
SymExpr::BuildZext { op, bits } => Some(bv!(op).zero_ext(u32::from(bits)).into()),
|
SymExpr::BoolToBits { op, bits } => Some(
|
||||||
SymExpr::BuildTrunc { op, bits } => {
|
|
||||||
Some(bv!(op).extract(u32::from(bits - 1), 0).into())
|
|
||||||
}
|
|
||||||
SymExpr::BuildBoolToBits { op, bits } => Some(
|
|
||||||
bool!(op)
|
bool!(op)
|
||||||
.ite(
|
.ite(
|
||||||
&BV::from_u64(&ctx, 1, u32::from(bits)),
|
&BV::from_u64(&ctx, 1, u32::from(bits)),
|
||||||
@ -227,29 +223,13 @@ fn generate_mutations(iter: impl Iterator<Item = (SymExprRef, SymExpr)>) -> Vec<
|
|||||||
)
|
)
|
||||||
.into(),
|
.into(),
|
||||||
),
|
),
|
||||||
SymExpr::ConcatHelper { a, b } => bv_binop!(a concat b),
|
SymExpr::Concat { a, b } => bv_binop!(a concat b),
|
||||||
SymExpr::ExtractHelper {
|
SymExpr::Extract {
|
||||||
op,
|
op,
|
||||||
first_bit,
|
first_bit,
|
||||||
last_bit,
|
last_bit,
|
||||||
} => Some(bv!(op).extract(first_bit as u32, last_bit as u32).into()),
|
} => Some(bv!(op).extract(first_bit as u32, last_bit as u32).into()),
|
||||||
SymExpr::BuildExtract {
|
SymExpr::Insert {
|
||||||
op,
|
|
||||||
offset,
|
|
||||||
length,
|
|
||||||
little_endian,
|
|
||||||
} => Some(build_extract(&(bv!(op)), offset, length, little_endian).into()),
|
|
||||||
SymExpr::BuildBswap { op } => {
|
|
||||||
let bv = bv!(op);
|
|
||||||
let bits = bv.get_size();
|
|
||||||
assert_eq!(
|
|
||||||
bits % 16,
|
|
||||||
0,
|
|
||||||
"bswap is only compatible with an even number of bvytes in the BV"
|
|
||||||
);
|
|
||||||
Some(build_extract(&bv, 0, u64::from(bits) / 8, true).into())
|
|
||||||
}
|
|
||||||
SymExpr::BuildInsert {
|
|
||||||
target,
|
target,
|
||||||
to_insert,
|
to_insert,
|
||||||
offset,
|
offset,
|
||||||
@ -297,7 +277,7 @@ fn generate_mutations(iter: impl Iterator<Item = (SymExprRef, SymExpr)>) -> Vec<
|
|||||||
};
|
};
|
||||||
if let Some(expr) = z3_expr {
|
if let Some(expr) = z3_expr {
|
||||||
translation.insert(id, expr);
|
translation.insert(id, expr);
|
||||||
} else if let SymExpr::PushPathConstraint {
|
} else if let SymExpr::PathConstraint {
|
||||||
constraint,
|
constraint,
|
||||||
site_id: _,
|
site_id: _,
|
||||||
taken,
|
taken,
|
||||||
|
@ -2,6 +2,7 @@
|
|||||||
name = "symcc_runtime"
|
name = "symcc_runtime"
|
||||||
version = "0.1.0"
|
version = "0.1.0"
|
||||||
edition = "2018"
|
edition = "2018"
|
||||||
|
authors = ["Julius Hohnerlein <julihoh@users.noreply.github.com>"]
|
||||||
|
|
||||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||||
|
|
||||||
|
@ -1,12 +1,21 @@
|
|||||||
|
//! [`Filter`]s are ergonomic abstractions over [`Runtime`] that facilitate filtering expressions.
|
||||||
|
|
||||||
use std::collections::HashSet;
|
use std::collections::HashSet;
|
||||||
|
|
||||||
#[allow(clippy::wildcard_imports)]
|
#[allow(clippy::wildcard_imports)]
|
||||||
use crate::*;
|
use crate::*;
|
||||||
|
|
||||||
|
mod coverage;
|
||||||
|
pub use coverage::{CallStackCoverage, HitmapFilter};
|
||||||
|
|
||||||
|
// creates the method declaration and default implementations for the filter trait
|
||||||
macro_rules! rust_filter_function_declaration {
|
macro_rules! rust_filter_function_declaration {
|
||||||
|
// expression_unreachable is not supported for filters
|
||||||
(pub fn expression_unreachable(expressions: *mut RSymExpr, num_elements: usize), $c_name:ident;) => {
|
(pub fn expression_unreachable(expressions: *mut RSymExpr, num_elements: usize), $c_name:ident;) => {
|
||||||
};
|
};
|
||||||
|
|
||||||
|
// push_path_constraint is not caught by the following case (because it has not return value),
|
||||||
|
// but still needs to return something
|
||||||
(pub fn push_path_constraint($( $arg:ident : $type:ty ),*$(,)?), $c_name:ident;) => {
|
(pub fn push_path_constraint($( $arg:ident : $type:ty ),*$(,)?), $c_name:ident;) => {
|
||||||
#[allow(unused_variables)]
|
#[allow(unused_variables)]
|
||||||
fn push_path_constraint(&mut self, $($arg : $type),*) -> bool {
|
fn push_path_constraint(&mut self, $($arg : $type),*) -> bool {
|
||||||
@ -25,18 +34,46 @@ macro_rules! rust_filter_function_declaration {
|
|||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
||||||
/// A [`Filter`] can decide for each expression whether the expression should be trace symbolically or be
|
/// A [`Filter`] can decide for each expression whether the expression should be traced symbolically or be
|
||||||
/// concretized. This allows to implement filtering mechanisms that reduce the amount of traced expressions by
|
/// concretized. This allows to implement filtering mechanisms that reduce the amount of traced expressions by
|
||||||
/// concretizing uninteresting expressions.
|
/// concretizing uninteresting expressions.
|
||||||
/// If a filter concretizes an expression that would have later been used as part of another expression that
|
/// If a filter concretizes an expression that would have later been used as part of another expression that
|
||||||
/// is still symbolic, a concrete instead of a symbolic value is received.
|
/// is still symbolic, a concrete instead of a symbolic value is received.
|
||||||
///
|
///
|
||||||
|
/// The interface for a filter matches [`Runtime`] with all methods returning `bool` instead of returning [`Option<RSymExpr>`].
|
||||||
|
/// Returning `true` indicates that the expression should _continue_ to be processed.
|
||||||
|
/// Returning `false` indicates that the expression should _not_ be processed any further and its result should be _concretized_.
|
||||||
|
///
|
||||||
/// For example:
|
/// For example:
|
||||||
/// Suppose there are symbolic expressions `a` and `b`. Expression `a` is concretized, `b` is still symbolic. If an add
|
/// Suppose there are symbolic expressions `a` and `b`. Expression `a` is concretized, `b` is still symbolic. If an add
|
||||||
/// operation between `a` and `b` is encountered, it will receive `a`'s concrete value and `b` as a symbolic expression.
|
/// operation between `a` and `b` is encountered, it will receive `a`'s concrete value and `b` as a symbolic expression.
|
||||||
///
|
///
|
||||||
/// An expression filter also receives code locations (`visit_*` methods) as they are visited in between operations
|
/// An expression filter also receives code locations (`visit_*` methods) as they are visited in between operations
|
||||||
/// and these code locations are typically used to decide whether an expression should be concretized.
|
/// and these code locations are typically used to decide whether an expression should be concretized.
|
||||||
|
///
|
||||||
|
/// ## How to use
|
||||||
|
/// To create your own filter, implement this trait for a new struct.
|
||||||
|
/// All methods of this trait have default implementations, so you can just implement those methods which you may want
|
||||||
|
/// to filter.
|
||||||
|
///
|
||||||
|
/// Use a [`FilterRuntime`] to compose your filter with a [`Runtime`].
|
||||||
|
/// ## Example
|
||||||
|
/// As an example, the following filter concretizes all variables (and, therefore, expressions based on these variables) that are not part of a predetermined set of variables.
|
||||||
|
/// It is also available to use as [`SelectiveSymbolication`].
|
||||||
|
/// ```no_run
|
||||||
|
/// # use symcc_runtime::filter::Filter;
|
||||||
|
/// # use std::collections::HashSet;
|
||||||
|
/// struct SelectiveSymbolication {
|
||||||
|
/// bytes_to_symbolize: HashSet<usize>,
|
||||||
|
/// }
|
||||||
|
///
|
||||||
|
/// impl Filter for SelectiveSymbolication {
|
||||||
|
/// fn get_input_byte(&mut self, offset: usize) -> bool {
|
||||||
|
/// self.bytes_to_symbolize.contains(&offset)
|
||||||
|
/// }
|
||||||
|
/// // Note: No need to implement methods that we are not interested in!
|
||||||
|
/// }
|
||||||
|
/// ```
|
||||||
pub trait Filter {
|
pub trait Filter {
|
||||||
invoke_macro_with_rust_runtime_exports!(rust_filter_function_declaration;);
|
invoke_macro_with_rust_runtime_exports!(rust_filter_function_declaration;);
|
||||||
}
|
}
|
||||||
@ -186,217 +223,3 @@ impl Filter for NoFloat {
|
|||||||
false
|
false
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
pub mod coverage {
|
|
||||||
use std::{
|
|
||||||
collections::hash_map::DefaultHasher,
|
|
||||||
convert::TryInto,
|
|
||||||
hash::{BuildHasher, BuildHasherDefault, Hash, Hasher},
|
|
||||||
marker::PhantomData,
|
|
||||||
};
|
|
||||||
|
|
||||||
use libafl::bolts::shmem::ShMem;
|
|
||||||
|
|
||||||
use super::Filter;
|
|
||||||
|
|
||||||
const MAP_SIZE: usize = 65536;
|
|
||||||
|
|
||||||
/// A coverage-based [`Filter`] based on the expression pruning from [`QSym`](https://github.com/sslab-gatech/qsym)
|
|
||||||
/// [here](https://github.com/sslab-gatech/qsym/blob/master/qsym/pintool/call_stack_manager.cpp).
|
|
||||||
struct CallStackCoverage<
|
|
||||||
THasher: Hasher = DefaultHasher,
|
|
||||||
THashBuilder: BuildHasher = BuildHasherDefault<THasher>,
|
|
||||||
> {
|
|
||||||
call_stack: Vec<usize>,
|
|
||||||
call_stack_hash: u64,
|
|
||||||
is_interesting: bool,
|
|
||||||
bitmap: Vec<u16>,
|
|
||||||
pending: bool,
|
|
||||||
last_location: usize,
|
|
||||||
hasher_builder: THashBuilder,
|
|
||||||
hasher_phantom: PhantomData<THasher>,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Default for CallStackCoverage<DefaultHasher, BuildHasherDefault<DefaultHasher>> {
|
|
||||||
fn default() -> Self {
|
|
||||||
Self {
|
|
||||||
call_stack: Vec::new(),
|
|
||||||
call_stack_hash: 0,
|
|
||||||
is_interesting: true,
|
|
||||||
bitmap: vec![0; MAP_SIZE],
|
|
||||||
pending: false,
|
|
||||||
last_location: 0,
|
|
||||||
hasher_builder: BuildHasherDefault::default(),
|
|
||||||
hasher_phantom: PhantomData,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<THasher: Hasher, THashBuilder: BuildHasher> CallStackCoverage<THasher, THashBuilder> {
|
|
||||||
pub fn visit_call(&mut self, location: usize) {
|
|
||||||
self.call_stack.push(location);
|
|
||||||
self.update_call_stack_hash();
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn visit_ret(&mut self, location: usize) {
|
|
||||||
if self.call_stack.is_empty() {
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
let num_elements_to_remove = self
|
|
||||||
.call_stack
|
|
||||||
.iter()
|
|
||||||
.rev()
|
|
||||||
.take_while(|&&loc| loc != location)
|
|
||||||
.count()
|
|
||||||
+ 1;
|
|
||||||
|
|
||||||
self.call_stack
|
|
||||||
.truncate(self.call_stack.len() - num_elements_to_remove);
|
|
||||||
self.update_call_stack_hash();
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn visit_basic_block(&mut self, location: usize) {
|
|
||||||
self.last_location = location;
|
|
||||||
self.pending = true;
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn is_interesting(&self) -> bool {
|
|
||||||
self.is_interesting
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn update_bitmap(&mut self) {
|
|
||||||
if self.pending {
|
|
||||||
self.pending = false;
|
|
||||||
|
|
||||||
let mut hasher = self.hasher_builder.build_hasher();
|
|
||||||
self.last_location.hash(&mut hasher);
|
|
||||||
self.call_stack_hash.hash(&mut hasher);
|
|
||||||
let hash = hasher.finish();
|
|
||||||
let index: usize = (hash % MAP_SIZE as u64).try_into().unwrap();
|
|
||||||
let value = self.bitmap[index] / 8;
|
|
||||||
self.is_interesting = value == 0 || value.is_power_of_two();
|
|
||||||
*self.bitmap.get_mut(index).unwrap() += 1;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn update_call_stack_hash(&mut self) {
|
|
||||||
let mut hasher = self.hasher_builder.build_hasher();
|
|
||||||
self.call_stack
|
|
||||||
.iter()
|
|
||||||
.for_each(|&loc| loc.hash(&mut hasher));
|
|
||||||
self.call_stack_hash = hasher.finish();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
macro_rules! call_stack_coverage_filter_function_implementation {
|
|
||||||
(pub fn expression_unreachable(expressions: *mut RSymExpr, num_elements: usize), $c_name:ident;) => {
|
|
||||||
};
|
|
||||||
|
|
||||||
(pub fn notify_basic_block(site_id: usize), $c_name:ident;) => {
|
|
||||||
fn notify_basic_block(&mut self, site_id: usize) {
|
|
||||||
self.visit_basic_block(site_id);
|
|
||||||
}
|
|
||||||
};
|
|
||||||
(pub fn notify_call(site_id: usize), $c_name:ident;) => {
|
|
||||||
fn notify_call(&mut self, site_id: usize) {
|
|
||||||
self.visit_call(site_id);
|
|
||||||
}
|
|
||||||
};
|
|
||||||
(pub fn notify_ret(site_id: usize), $c_name:ident;) => {
|
|
||||||
fn notify_ret(&mut self, site_id: usize) {
|
|
||||||
self.visit_ret(site_id);
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
(pub fn push_path_constraint($( $arg:ident : $type:ty ),*$(,)?), $c_name:ident;) => {
|
|
||||||
fn push_path_constraint(&mut self, $( _ : $type ),*) -> bool {
|
|
||||||
self.update_bitmap();
|
|
||||||
self.is_interesting()
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
(pub fn $name:ident($( $arg:ident : $type:ty ),*$(,)?) -> $ret:ty, $c_name:ident;) => {
|
|
||||||
fn $name(&mut self, $( _ : $type),*) -> bool {
|
|
||||||
self.update_bitmap();
|
|
||||||
self.is_interesting()
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
(pub fn $name:ident($( $arg:ident : $type:ty ),*$(,)?), $c_name:ident;) => {
|
|
||||||
fn $name(&mut self, $( _ : $type),*) {
|
|
||||||
}
|
|
||||||
};
|
|
||||||
}
|
|
||||||
|
|
||||||
#[allow(clippy::wildcard_imports)]
|
|
||||||
use crate::*;
|
|
||||||
|
|
||||||
impl<THasher: Hasher, THashBuilder: BuildHasher> Filter
|
|
||||||
for CallStackCoverage<THasher, THashBuilder>
|
|
||||||
{
|
|
||||||
invoke_macro_with_rust_runtime_exports!(call_stack_coverage_filter_function_implementation;);
|
|
||||||
}
|
|
||||||
|
|
||||||
/// A [`Filter`] that just observers Basic Block locations and updates a given Hitmap as a [`ShMem`].
|
|
||||||
pub struct HitmapFilter<M, BH: BuildHasher = BuildHasherDefault<DefaultHasher>> {
|
|
||||||
hitcounts_map: M,
|
|
||||||
build_hasher: BH,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<M> HitmapFilter<M, BuildHasherDefault<DefaultHasher>>
|
|
||||||
where
|
|
||||||
M: ShMem,
|
|
||||||
{
|
|
||||||
/// Creates a new `HitmapFilter` using the given map and the [`DefaultHasher`].
|
|
||||||
pub fn new(hitcounts_map: M) -> Self {
|
|
||||||
Self::new_with_default_hasher_builder(hitcounts_map)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<M, H> HitmapFilter<M, BuildHasherDefault<H>>
|
|
||||||
where
|
|
||||||
M: ShMem,
|
|
||||||
H: Hasher + Default,
|
|
||||||
{
|
|
||||||
/// Creates a new `HitmapFilter` using the given map and [`Hasher`] (as type argument) using the [`BuildHasherDefault`].
|
|
||||||
pub fn new_with_default_hasher_builder(hitcounts_map: M) -> Self {
|
|
||||||
Self::new_with_build_hasher(hitcounts_map, BuildHasherDefault::default())
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<M, BH> HitmapFilter<M, BH>
|
|
||||||
where
|
|
||||||
M: ShMem,
|
|
||||||
BH: BuildHasher,
|
|
||||||
{
|
|
||||||
/// Creates a new `HitmapFilter` using the given map and [`BuildHasher`] (as type argument).
|
|
||||||
pub fn new_with_build_hasher(hitcounts_map: M, build_hasher: BH) -> Self {
|
|
||||||
Self {
|
|
||||||
hitcounts_map,
|
|
||||||
build_hasher,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn register_location_on_hitmap(&mut self, location: usize) {
|
|
||||||
let mut hasher = self.build_hasher.build_hasher();
|
|
||||||
location.hash(&mut hasher);
|
|
||||||
let hash = (hasher.finish() % usize::MAX as u64) as usize;
|
|
||||||
let val = unsafe {
|
|
||||||
// SAFETY: the index is modulo by the length, therefore it is always in bounds
|
|
||||||
let len = self.hitcounts_map.len();
|
|
||||||
self.hitcounts_map.map_mut().get_unchecked_mut(hash % len)
|
|
||||||
};
|
|
||||||
*val = val.saturating_add(1);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<M, BH> Filter for HitmapFilter<M, BH>
|
|
||||||
where
|
|
||||||
M: ShMem,
|
|
||||||
BH: BuildHasher,
|
|
||||||
{
|
|
||||||
fn notify_basic_block(&mut self, location_id: usize) {
|
|
||||||
self.register_location_on_hitmap(location_id);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
212
libafl_concolic/symcc_runtime/src/filter/coverage.rs
Normal file
212
libafl_concolic/symcc_runtime/src/filter/coverage.rs
Normal file
@ -0,0 +1,212 @@
|
|||||||
|
use std::{
|
||||||
|
collections::hash_map::DefaultHasher,
|
||||||
|
convert::TryInto,
|
||||||
|
hash::{BuildHasher, BuildHasherDefault, Hash, Hasher},
|
||||||
|
marker::PhantomData,
|
||||||
|
};
|
||||||
|
|
||||||
|
use libafl::bolts::shmem::ShMem;
|
||||||
|
|
||||||
|
use super::Filter;
|
||||||
|
|
||||||
|
const MAP_SIZE: usize = 65536;
|
||||||
|
|
||||||
|
/// A coverage-based [`Filter`] based on the
|
||||||
|
/// [expression pruning](https://github.com/sslab-gatech/qsym/blob/master/qsym/pintool/call_stack_manager.cpp) from
|
||||||
|
/// [`QSym`](https://github.com/sslab-gatech/qsym).
|
||||||
|
pub struct CallStackCoverage<
|
||||||
|
THasher: Hasher = DefaultHasher,
|
||||||
|
THashBuilder: BuildHasher = BuildHasherDefault<THasher>,
|
||||||
|
> {
|
||||||
|
call_stack: Vec<usize>,
|
||||||
|
call_stack_hash: u64,
|
||||||
|
is_interesting: bool,
|
||||||
|
bitmap: Vec<u16>,
|
||||||
|
pending: bool,
|
||||||
|
last_location: usize,
|
||||||
|
hasher_builder: THashBuilder,
|
||||||
|
hasher_phantom: PhantomData<THasher>,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl Default for CallStackCoverage<DefaultHasher, BuildHasherDefault<DefaultHasher>> {
|
||||||
|
fn default() -> Self {
|
||||||
|
Self {
|
||||||
|
call_stack: Vec::new(),
|
||||||
|
call_stack_hash: 0,
|
||||||
|
is_interesting: true,
|
||||||
|
bitmap: vec![0; MAP_SIZE],
|
||||||
|
pending: false,
|
||||||
|
last_location: 0,
|
||||||
|
hasher_builder: BuildHasherDefault::default(),
|
||||||
|
hasher_phantom: PhantomData,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<THasher: Hasher, THashBuilder: BuildHasher> CallStackCoverage<THasher, THashBuilder> {
|
||||||
|
pub fn visit_call(&mut self, location: usize) {
|
||||||
|
self.call_stack.push(location);
|
||||||
|
self.update_call_stack_hash();
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn visit_ret(&mut self, location: usize) {
|
||||||
|
if self.call_stack.is_empty() {
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
let num_elements_to_remove = self
|
||||||
|
.call_stack
|
||||||
|
.iter()
|
||||||
|
.rev()
|
||||||
|
.take_while(|&&loc| loc != location)
|
||||||
|
.count()
|
||||||
|
+ 1;
|
||||||
|
|
||||||
|
self.call_stack
|
||||||
|
.truncate(self.call_stack.len() - num_elements_to_remove);
|
||||||
|
self.update_call_stack_hash();
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn visit_basic_block(&mut self, location: usize) {
|
||||||
|
self.last_location = location;
|
||||||
|
self.pending = true;
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn is_interesting(&self) -> bool {
|
||||||
|
self.is_interesting
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn update_bitmap(&mut self) {
|
||||||
|
if self.pending {
|
||||||
|
self.pending = false;
|
||||||
|
|
||||||
|
let mut hasher = self.hasher_builder.build_hasher();
|
||||||
|
self.last_location.hash(&mut hasher);
|
||||||
|
self.call_stack_hash.hash(&mut hasher);
|
||||||
|
let hash = hasher.finish();
|
||||||
|
let index: usize = (hash % MAP_SIZE as u64).try_into().unwrap();
|
||||||
|
let value = self.bitmap[index] / 8;
|
||||||
|
self.is_interesting = value == 0 || value.is_power_of_two();
|
||||||
|
*self.bitmap.get_mut(index).unwrap() += 1;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn update_call_stack_hash(&mut self) {
|
||||||
|
let mut hasher = self.hasher_builder.build_hasher();
|
||||||
|
self.call_stack
|
||||||
|
.iter()
|
||||||
|
.for_each(|&loc| loc.hash(&mut hasher));
|
||||||
|
self.call_stack_hash = hasher.finish();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
macro_rules! call_stack_coverage_filter_function_implementation {
|
||||||
|
(pub fn expression_unreachable(expressions: *mut RSymExpr, num_elements: usize), $c_name:ident;) => {
|
||||||
|
};
|
||||||
|
|
||||||
|
(pub fn notify_basic_block(site_id: usize), $c_name:ident;) => {
|
||||||
|
fn notify_basic_block(&mut self, site_id: usize) {
|
||||||
|
self.visit_basic_block(site_id);
|
||||||
|
}
|
||||||
|
};
|
||||||
|
(pub fn notify_call(site_id: usize), $c_name:ident;) => {
|
||||||
|
fn notify_call(&mut self, site_id: usize) {
|
||||||
|
self.visit_call(site_id);
|
||||||
|
}
|
||||||
|
};
|
||||||
|
(pub fn notify_ret(site_id: usize), $c_name:ident;) => {
|
||||||
|
fn notify_ret(&mut self, site_id: usize) {
|
||||||
|
self.visit_ret(site_id);
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
(pub fn push_path_constraint($( $arg:ident : $type:ty ),*$(,)?), $c_name:ident;) => {
|
||||||
|
fn push_path_constraint(&mut self, $( _ : $type ),*) -> bool {
|
||||||
|
self.update_bitmap();
|
||||||
|
self.is_interesting()
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
(pub fn $name:ident($( $arg:ident : $type:ty ),*$(,)?) -> $ret:ty, $c_name:ident;) => {
|
||||||
|
fn $name(&mut self, $( _ : $type),*) -> bool {
|
||||||
|
self.update_bitmap();
|
||||||
|
self.is_interesting()
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
(pub fn $name:ident($( $arg:ident : $type:ty ),*$(,)?), $c_name:ident;) => {
|
||||||
|
fn $name(&mut self, $( _ : $type),*) {
|
||||||
|
}
|
||||||
|
};
|
||||||
|
}
|
||||||
|
|
||||||
|
#[allow(clippy::wildcard_imports)]
|
||||||
|
use crate::*;
|
||||||
|
|
||||||
|
impl<THasher: Hasher, THashBuilder: BuildHasher> Filter
|
||||||
|
for CallStackCoverage<THasher, THashBuilder>
|
||||||
|
{
|
||||||
|
invoke_macro_with_rust_runtime_exports!(call_stack_coverage_filter_function_implementation;);
|
||||||
|
}
|
||||||
|
|
||||||
|
/// A [`Filter`] that just observes Basic Block locations and updates a given Hitmap as a [`ShMem`].
|
||||||
|
pub struct HitmapFilter<M, BH: BuildHasher = BuildHasherDefault<DefaultHasher>> {
|
||||||
|
hitcounts_map: M,
|
||||||
|
build_hasher: BH,
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<M> HitmapFilter<M, BuildHasherDefault<DefaultHasher>>
|
||||||
|
where
|
||||||
|
M: ShMem,
|
||||||
|
{
|
||||||
|
/// Creates a new `HitmapFilter` using the given map and the [`DefaultHasher`].
|
||||||
|
pub fn new(hitcounts_map: M) -> Self {
|
||||||
|
Self::new_with_default_hasher_builder(hitcounts_map)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<M, H> HitmapFilter<M, BuildHasherDefault<H>>
|
||||||
|
where
|
||||||
|
M: ShMem,
|
||||||
|
H: Hasher + Default,
|
||||||
|
{
|
||||||
|
/// Creates a new `HitmapFilter` using the given map and [`Hasher`] (as type argument) using the [`BuildHasherDefault`].
|
||||||
|
pub fn new_with_default_hasher_builder(hitcounts_map: M) -> Self {
|
||||||
|
Self::new_with_build_hasher(hitcounts_map, BuildHasherDefault::default())
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<M, BH> HitmapFilter<M, BH>
|
||||||
|
where
|
||||||
|
M: ShMem,
|
||||||
|
BH: BuildHasher,
|
||||||
|
{
|
||||||
|
/// Creates a new `HitmapFilter` using the given map and [`BuildHasher`] (as type argument).
|
||||||
|
pub fn new_with_build_hasher(hitcounts_map: M, build_hasher: BH) -> Self {
|
||||||
|
Self {
|
||||||
|
hitcounts_map,
|
||||||
|
build_hasher,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn register_location_on_hitmap(&mut self, location: usize) {
|
||||||
|
let mut hasher = self.build_hasher.build_hasher();
|
||||||
|
location.hash(&mut hasher);
|
||||||
|
let hash = (hasher.finish() % usize::MAX as u64) as usize;
|
||||||
|
let val = unsafe {
|
||||||
|
// SAFETY: the index is modulo by the length, therefore it is always in bounds
|
||||||
|
let len = self.hitcounts_map.len();
|
||||||
|
self.hitcounts_map.map_mut().get_unchecked_mut(hash % len)
|
||||||
|
};
|
||||||
|
*val = val.saturating_add(1);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<M, BH> Filter for HitmapFilter<M, BH>
|
||||||
|
where
|
||||||
|
M: ShMem,
|
||||||
|
BH: BuildHasher,
|
||||||
|
{
|
||||||
|
fn notify_basic_block(&mut self, location_id: usize) {
|
||||||
|
self.register_location_on_hitmap(location_id);
|
||||||
|
}
|
||||||
|
}
|
@ -1,6 +1,36 @@
|
|||||||
|
//! # `SymCC` Runtime Bindings
|
||||||
|
//! This crate contains bindings to the [`SymCC`](https://github.com/eurecom-s3/symcc) [runtime interface](https://github.com/eurecom-s3/symcc/blob/master/runtime/RuntimeCommon.h) to be used from Rust.
|
||||||
|
//! A `SymCC` runtime can be used with either `SymCC` or [`SymQEMU`](https://github.com/eurecom-s3/symqemu) to trace the execution of a target program.
|
||||||
|
//!
|
||||||
|
//! ## How to use
|
||||||
|
//! On a high level, users of this crate can implement the [`Runtime`] trait and export the runtime interface as a `cdylib` using the [`export_runtime`] macro.
|
||||||
|
//! On a technical level, a `SymCC` runtime is a dynamic library (/shared object) that exposes a set of symbols that the instrumentation layer of `SymCC` calls into during execution of the target.
|
||||||
|
//! Therefore, to create a runtime, a separate crate for the runtime is required, because this is the only way to create a separate dynamic library using cargo.
|
||||||
|
//!
|
||||||
|
//! ## Goodies
|
||||||
|
//! To facilitate common use cases, this crate also contains some pre-built functionality in the form of a [`tracing::TracingRuntime`] that traces the execution to a shared memory region.
|
||||||
|
//! It also contains a separate abstraction to easily filter the expressions that make up such a trace in the [`filter`] module.
|
||||||
|
//! For example, it contains a [`filter::NoFloat`] filter that concretizes all floating point operations in the trace, because those are usually more difficult to handle than discrete constraints.
|
||||||
|
//!
|
||||||
|
//! ## Crate setup
|
||||||
|
//! Your runtime crate should have the following keys set in its `Cargo.toml`:
|
||||||
|
//! ```toml
|
||||||
|
//! [profile.release]
|
||||||
|
//! # this is somewhat important to ensure the runtime does not unwind into the target program.
|
||||||
|
//! panic = "abort"
|
||||||
|
//! [profile.debug]
|
||||||
|
//! panic = "abort"
|
||||||
|
//!
|
||||||
|
//! [lib]
|
||||||
|
//! # this is required for the output to be a shared object (.so file)
|
||||||
|
//! crate-type = ["cdylib"]
|
||||||
|
//! # SymCC and SymQEMU expect to runtime file to be called `libSymRuntime.so`. Setting the name to `SymRuntime` achieves this.
|
||||||
|
//! name = "SymRuntime"
|
||||||
|
//! ```
|
||||||
pub mod filter;
|
pub mod filter;
|
||||||
pub mod tracing;
|
pub mod tracing;
|
||||||
|
|
||||||
|
// The following exports are used by the `export_runtime` macro. They are therefore exported, but hidden from docs, as they are not supposed to be used directly by the user.
|
||||||
#[doc(hidden)]
|
#[doc(hidden)]
|
||||||
#[cfg(target_os = "linux")]
|
#[cfg(target_os = "linux")]
|
||||||
pub mod cpp_runtime {
|
pub mod cpp_runtime {
|
||||||
@ -49,8 +79,31 @@ macro_rules! rust_runtime_function_declaration {
|
|||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Values of this type identify an expression. They can be thought of as references to expressions.
|
||||||
|
///
|
||||||
|
/// All values of this type are produced by the `build_*` methods on [`Runtime`] and subsequently consumed by the runtime.
|
||||||
|
/// Therefore, how these values are interpreted is entirely up to the runtime.
|
||||||
|
/// They are pointer-sized and are required to be non-zero.
|
||||||
|
/// Therefore this type resolves to [`core::num::NonZeroUsize`].
|
||||||
pub type RSymExpr = concolic::SymExprRef;
|
pub type RSymExpr = concolic::SymExprRef;
|
||||||
|
|
||||||
|
/// This trait encapsulates the full interface of a runtime.
|
||||||
|
/// The individual methods of this trait are not documented, but follow a simple rules:
|
||||||
|
///
|
||||||
|
/// 1. methods starting with `build_` or end in `_helper` create new expressions in the trace
|
||||||
|
/// 2. `Runtime::get_input_byte` creates variable expressions
|
||||||
|
/// 3. methods starting with `notify_` trace give an indication as to where in the code the execution is at (using random, but stable identifiers)
|
||||||
|
/// 4. `Runtime::push_path_constraint` creates a root expression (no other expressions can reference this) and marks a path constraint in the execution of the target
|
||||||
|
/// 5. `Runtime::expression_unreachable` is called regularly to with [`RSymExpr`]'s that won't be referenced in future calls to the runtime (because they are not reachable anymore)
|
||||||
|
///
|
||||||
|
/// All methods that create new expressions return `Option<RSymExpr>`. Returning `Option::None` will concretize the result of the expression.
|
||||||
|
/// For example, returning `None` from `Runtime::build_udiv` will concretize the result of all unsidned integer division operations.
|
||||||
|
/// Filtering expressions like this is also facilitated by [`filter::Filter`].
|
||||||
|
///
|
||||||
|
/// ## Drop
|
||||||
|
/// The code generated from `export_runtime` will attempt to drop your runtime.
|
||||||
|
/// In the context of fuzzing it is expected that the process may crash and in this case, the runtime will not be dropped.
|
||||||
|
/// Therefore, any runtime should make sure to handle this case properly (for example by flushing buffers regularly).
|
||||||
pub trait Runtime {
|
pub trait Runtime {
|
||||||
invoke_macro_with_rust_runtime_exports!(rust_runtime_function_declaration;);
|
invoke_macro_with_rust_runtime_exports!(rust_runtime_function_declaration;);
|
||||||
}
|
}
|
||||||
@ -73,9 +126,11 @@ macro_rules! unwrap_option {
|
|||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Creates an exported extern C function for the given runtime function declaration, forwarding to the runtime as obtained by $rt_cb (which should be `fn (fn (&mut impl Runtime))`).
|
||||||
#[doc(hidden)]
|
#[doc(hidden)]
|
||||||
#[macro_export]
|
#[macro_export]
|
||||||
macro_rules! export_rust_runtime_fn {
|
macro_rules! export_rust_runtime_fn {
|
||||||
|
// special case for expression_unreachable, because we need to be convert pointer+length to slice
|
||||||
(pub fn expression_unreachable(expressions: *mut RSymExpr, num_elements: usize), $c_name:ident; $rt_cb:path) => {
|
(pub fn expression_unreachable(expressions: *mut RSymExpr, num_elements: usize), $c_name:ident; $rt_cb:path) => {
|
||||||
#[allow(clippy::missing_safety_doc)]
|
#[allow(clippy::missing_safety_doc)]
|
||||||
#[no_mangle]
|
#[no_mangle]
|
||||||
@ -86,6 +141,7 @@ macro_rules! export_rust_runtime_fn {
|
|||||||
})
|
})
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
// special case for push_path_constraint, we are not returning a new expression while taking an expression as argument
|
||||||
(pub fn push_path_constraint(constraint: RSymExpr, taken: bool, site_id: usize), $c_name:ident; $rt_cb:path) => {
|
(pub fn push_path_constraint(constraint: RSymExpr, taken: bool, site_id: usize), $c_name:ident; $rt_cb:path) => {
|
||||||
#[allow(clippy::missing_safety_doc)]
|
#[allow(clippy::missing_safety_doc)]
|
||||||
#[no_mangle]
|
#[no_mangle]
|
||||||
@ -97,6 +153,7 @@ macro_rules! export_rust_runtime_fn {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
// all other methods are handled by this
|
||||||
(pub fn $name:ident($( $arg:ident : $(::)?$($type:ident)::+ ),*$(,)?)$( -> $($ret:ident)::+)?, $c_name:ident; $rt_cb:path) => {
|
(pub fn $name:ident($( $arg:ident : $(::)?$($type:ident)::+ ),*$(,)?)$( -> $($ret:ident)::+)?, $c_name:ident; $rt_cb:path) => {
|
||||||
#[allow(clippy::missing_safety_doc)]
|
#[allow(clippy::missing_safety_doc)]
|
||||||
#[no_mangle]
|
#[no_mangle]
|
||||||
@ -109,7 +166,9 @@ macro_rules! export_rust_runtime_fn {
|
|||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// implements the [`NopRuntime`] methods by returning [`Default::default`] from all methods.
|
||||||
macro_rules! impl_nop_runtime_fn {
|
macro_rules! impl_nop_runtime_fn {
|
||||||
|
// special case for expression_unreachable, because it has a different signature in our runtime trait than in the c interface.
|
||||||
(pub fn expression_unreachable(expressions: *mut RSymExpr, num_elements: usize), $c_name:ident;) => {
|
(pub fn expression_unreachable(expressions: *mut RSymExpr, num_elements: usize), $c_name:ident;) => {
|
||||||
#[allow(clippy::default_trait_access)]
|
#[allow(clippy::default_trait_access)]
|
||||||
fn expression_unreachable(&mut self, _exprs: &[RSymExpr]) {std::default::Default::default()}
|
fn expression_unreachable(&mut self, _exprs: &[RSymExpr]) {std::default::Default::default()}
|
||||||
@ -121,36 +180,79 @@ macro_rules! impl_nop_runtime_fn {
|
|||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// This runtime does nothing and concretizes all expressions. Intended for testing purposes.
|
||||||
pub struct NopRuntime;
|
pub struct NopRuntime;
|
||||||
|
|
||||||
impl Runtime for NopRuntime {
|
impl Runtime for NopRuntime {
|
||||||
invoke_macro_with_rust_runtime_exports!(impl_nop_runtime_fn;);
|
invoke_macro_with_rust_runtime_exports!(impl_nop_runtime_fn;);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// This macro allows you to export your runtime from your crate. It is necessary to call this macro in your crate to get a functional runtime.
|
||||||
|
///
|
||||||
|
/// ## Simple form
|
||||||
|
/// The simplest invocation of this macro looks like this:
|
||||||
|
/// ```no_run
|
||||||
|
/// # #[macro_use] extern crate symcc_runtime;
|
||||||
|
/// # use symcc_runtime::{NopRuntime, Runtime};
|
||||||
|
/// export_runtime!(NopRuntime => NopRuntime);
|
||||||
|
/// ```
|
||||||
|
/// The first argument is an expression that constructs your `Runtime` type and the second argument is the name of your `Runtime` type.
|
||||||
|
/// For example, to construct a tracing runtime, the invocation would look like this:
|
||||||
|
/// ```no_run
|
||||||
|
/// # #[macro_use] extern crate symcc_runtime;
|
||||||
|
/// # use symcc_runtime::{tracing::TracingRuntime, Runtime};
|
||||||
|
/// export_runtime!(TracingRuntime::new(todo!()) => TracingRuntime);
|
||||||
|
/// ```
|
||||||
|
///
|
||||||
|
/// ## Runtime composition using `Filter`s
|
||||||
|
/// If you're not a fan of macro magic, you should stop reading here.
|
||||||
|
///
|
||||||
|
/// To construct a runtime that is composed of [`filter::Filter`]s, you can save some boilerplate code by using the extended form of this macro.
|
||||||
|
/// The gist of it is that you can prepend any number of `constructor => type` statements (separated by `;`) to your final runtime statement and the result of this macro will wrap your final runtime with the given filters.
|
||||||
|
/// Filters are applied from left to right.
|
||||||
|
///
|
||||||
|
/// Example:
|
||||||
|
/// ```no_run
|
||||||
|
/// # #[macro_use] extern crate symcc_runtime;
|
||||||
|
/// # use symcc_runtime::{tracing::TracingRuntime, Runtime, filter::NoFloat};
|
||||||
|
/// export_runtime!(NoFloat => NoFloat; TracingRuntime::new(todo!()) => TracingRuntime);
|
||||||
|
/// ```
|
||||||
|
/// This will construct a runtime that is first filtered by [`filter::NoFloat`] and then traced by the tracing runtime.
|
||||||
|
///
|
||||||
|
/// You can achieve the same effect by constructing [`filter::FilterRuntime`] manually, but as you add more filters, the types become tedious to write out.
|
||||||
#[macro_export]
|
#[macro_export]
|
||||||
macro_rules! export_runtime {
|
macro_rules! export_runtime {
|
||||||
($filter_constructor:expr => $filter:ty ; $($constructor:expr => $rt:ty);+) => {
|
// Simple version: just export this runtime
|
||||||
export_runtime!(@final export_runtime!(@combine_constructor $filter_constructor; $($constructor);+) => export_runtime!(@combine_type $filter; $($rt);+));
|
|
||||||
};
|
|
||||||
|
|
||||||
($constructor:expr => $rt:ty) => {
|
($constructor:expr => $rt:ty) => {
|
||||||
export_runtime!(@final $constructor => $rt);
|
export_runtime!(@final $constructor => $rt);
|
||||||
};
|
};
|
||||||
|
|
||||||
|
// Compositional version: export this chain of filters and a final runtime
|
||||||
|
($filter_constructor:expr => $filter:ty ; $($constructor:expr => $rt:ty);+) => {
|
||||||
|
export_runtime!(@final export_runtime!(@combine_constructor $filter_constructor; $($constructor);+) => export_runtime!(@combine_type $filter; $($rt);+));
|
||||||
|
};
|
||||||
|
|
||||||
|
// combines a chain of filter constructor expressions
|
||||||
|
// recursive case: wrap the constructor expression in a `filter::FilterRuntime::new`
|
||||||
(@combine_constructor $filter_constructor:expr ; $($constructor:expr);+) => {
|
(@combine_constructor $filter_constructor:expr ; $($constructor:expr);+) => {
|
||||||
$crate::filter::FilterRuntime::new($filter_constructor, export_runtime!(@combine_constructor $($constructor);+))
|
$crate::filter::FilterRuntime::new($filter_constructor, export_runtime!(@combine_constructor $($constructor);+))
|
||||||
};
|
};
|
||||||
|
// base case
|
||||||
(@combine_constructor $constructor:expr) => {
|
(@combine_constructor $constructor:expr) => {
|
||||||
$constructor
|
$constructor
|
||||||
};
|
};
|
||||||
|
|
||||||
|
// combines a chain of filter type expressions
|
||||||
|
// recursive case: wrap the type in a `filter::FilterRuntime`
|
||||||
(@combine_type $filter:ty ; $($rt:ty);+) => {
|
(@combine_type $filter:ty ; $($rt:ty);+) => {
|
||||||
$crate::filter::FilterRuntime<$filter, export_runtime!(@combine_type $($rt);+)>
|
$crate::filter::FilterRuntime<$filter, export_runtime!(@combine_type $($rt);+)>
|
||||||
};
|
};
|
||||||
|
// base case
|
||||||
(@combine_type $rt:ty) => {
|
(@combine_type $rt:ty) => {
|
||||||
$rt
|
$rt
|
||||||
};
|
};
|
||||||
|
|
||||||
|
// finally, generate the necessary code for the given runtime
|
||||||
(@final $constructor:expr => $rt:ty) => {
|
(@final $constructor:expr => $rt:ty) => {
|
||||||
// We are creating a piece of shared mutable state here for our runtime, which is used unsafely.
|
// We are creating a piece of shared mutable state here for our runtime, which is used unsafely.
|
||||||
// The correct solution here would be to either use a mutex or have per-thread state,
|
// The correct solution here would be to either use a mutex or have per-thread state,
|
||||||
|
@ -1,14 +1,18 @@
|
|||||||
pub use libafl::observers::concolic::{
|
//! Tracing of expressions in a serialized form.
|
||||||
serialization_format::shared_memory::StdShMemMessageFileWriter, SymExpr,
|
|
||||||
};
|
pub use libafl::observers::concolic::serialization_format::StdShMemMessageFileWriter;
|
||||||
|
use libafl::observers::concolic::SymExpr;
|
||||||
|
|
||||||
use crate::{RSymExpr, Runtime};
|
use crate::{RSymExpr, Runtime};
|
||||||
|
|
||||||
|
/// Traces the expressions according to the format described in [`libafl::observers::concolic::serialization_format`].
|
||||||
|
/// The format can be read from elsewhere to perform processing of the expressions outside of the runtime.
|
||||||
pub struct TracingRuntime {
|
pub struct TracingRuntime {
|
||||||
writer: StdShMemMessageFileWriter,
|
writer: StdShMemMessageFileWriter,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl TracingRuntime {
|
impl TracingRuntime {
|
||||||
|
/// Creates the runtime, tracing using the given writer.
|
||||||
#[must_use]
|
#[must_use]
|
||||||
pub fn new(writer: StdShMemMessageFileWriter) -> Self {
|
pub fn new(writer: StdShMemMessageFileWriter) -> Self {
|
||||||
Self { writer }
|
Self { writer }
|
||||||
@ -52,101 +56,92 @@ macro_rules! binary_expression_builder {
|
|||||||
}
|
}
|
||||||
|
|
||||||
impl Runtime for TracingRuntime {
|
impl Runtime for TracingRuntime {
|
||||||
expression_builder!(get_input_byte(offset: usize) => GetInputByte);
|
expression_builder!(get_input_byte(offset: usize) => InputByte);
|
||||||
|
|
||||||
expression_builder!(build_integer(value: u64, bits: u8) => BuildInteger);
|
expression_builder!(build_integer(value: u64, bits: u8) => Integer);
|
||||||
expression_builder!(build_integer128(high: u64, low: u64) => BuildInteger128);
|
expression_builder!(build_integer128(high: u64, low: u64) => Integer128);
|
||||||
expression_builder!(build_float(value: f64, is_double: bool) => BuildFloat);
|
expression_builder!(build_float(value: f64, is_double: bool) => Float);
|
||||||
expression_builder!(build_null_pointer() => BuildNullPointer);
|
expression_builder!(build_null_pointer() => NullPointer);
|
||||||
expression_builder!(build_true() => BuildTrue);
|
expression_builder!(build_true() => True);
|
||||||
expression_builder!(build_false() => BuildFalse);
|
expression_builder!(build_false() => False);
|
||||||
expression_builder!(build_bool(value: bool) => BuildBool);
|
expression_builder!(build_bool(value: bool) => Bool);
|
||||||
|
|
||||||
unary_expression_builder!(build_neg, BuildNeg);
|
unary_expression_builder!(build_neg, Neg);
|
||||||
|
|
||||||
binary_expression_builder!(build_add, BuildAdd);
|
binary_expression_builder!(build_add, Add);
|
||||||
binary_expression_builder!(build_sub, BuildSub);
|
binary_expression_builder!(build_sub, Sub);
|
||||||
binary_expression_builder!(build_mul, BuildMul);
|
binary_expression_builder!(build_mul, Mul);
|
||||||
binary_expression_builder!(build_unsigned_div, BuildUnsignedDiv);
|
binary_expression_builder!(build_unsigned_div, UnsignedDiv);
|
||||||
binary_expression_builder!(build_signed_div, BuildSignedDiv);
|
binary_expression_builder!(build_signed_div, SignedDiv);
|
||||||
binary_expression_builder!(build_unsigned_rem, BuildUnsignedRem);
|
binary_expression_builder!(build_unsigned_rem, UnsignedRem);
|
||||||
binary_expression_builder!(build_signed_rem, BuildSignedRem);
|
binary_expression_builder!(build_signed_rem, SignedRem);
|
||||||
binary_expression_builder!(build_shift_left, BuildShiftLeft);
|
binary_expression_builder!(build_shift_left, ShiftLeft);
|
||||||
binary_expression_builder!(build_logical_shift_right, BuildLogicalShiftRight);
|
binary_expression_builder!(build_logical_shift_right, LogicalShiftRight);
|
||||||
binary_expression_builder!(build_arithmetic_shift_right, BuildArithmeticShiftRight);
|
binary_expression_builder!(build_arithmetic_shift_right, ArithmeticShiftRight);
|
||||||
|
|
||||||
binary_expression_builder!(build_signed_less_than, BuildSignedLessThan);
|
binary_expression_builder!(build_signed_less_than, SignedLessThan);
|
||||||
binary_expression_builder!(build_signed_less_equal, BuildSignedLessEqual);
|
binary_expression_builder!(build_signed_less_equal, SignedLessEqual);
|
||||||
binary_expression_builder!(build_signed_greater_than, BuildSignedGreaterThan);
|
binary_expression_builder!(build_signed_greater_than, SignedGreaterThan);
|
||||||
binary_expression_builder!(build_signed_greater_equal, BuildSignedGreaterEqual);
|
binary_expression_builder!(build_signed_greater_equal, SignedGreaterEqual);
|
||||||
binary_expression_builder!(build_unsigned_less_than, BuildUnsignedLessThan);
|
binary_expression_builder!(build_unsigned_less_than, UnsignedLessThan);
|
||||||
binary_expression_builder!(build_unsigned_less_equal, BuildUnsignedLessEqual);
|
binary_expression_builder!(build_unsigned_less_equal, UnsignedLessEqual);
|
||||||
binary_expression_builder!(build_unsigned_greater_than, BuildUnsignedGreaterThan);
|
binary_expression_builder!(build_unsigned_greater_than, UnsignedGreaterThan);
|
||||||
binary_expression_builder!(build_unsigned_greater_equal, BuildUnsignedGreaterEqual);
|
binary_expression_builder!(build_unsigned_greater_equal, UnsignedGreaterEqual);
|
||||||
|
|
||||||
binary_expression_builder!(build_and, BuildAnd);
|
binary_expression_builder!(build_and, And);
|
||||||
binary_expression_builder!(build_or, BuildOr);
|
binary_expression_builder!(build_or, Or);
|
||||||
binary_expression_builder!(build_xor, BuildXor);
|
binary_expression_builder!(build_xor, Xor);
|
||||||
|
|
||||||
binary_expression_builder!(build_float_ordered, BuildFloatOrdered);
|
binary_expression_builder!(build_float_ordered, FloatOrdered);
|
||||||
binary_expression_builder!(
|
binary_expression_builder!(build_float_ordered_greater_than, FloatOrderedGreaterThan);
|
||||||
build_float_ordered_greater_than,
|
binary_expression_builder!(build_float_ordered_greater_equal, FloatOrderedGreaterEqual);
|
||||||
BuildFloatOrderedGreaterThan
|
binary_expression_builder!(build_float_ordered_less_than, FloatOrderedLessThan);
|
||||||
);
|
binary_expression_builder!(build_float_ordered_less_equal, FloatOrderedLessEqual);
|
||||||
binary_expression_builder!(
|
binary_expression_builder!(build_float_ordered_equal, FloatOrderedEqual);
|
||||||
build_float_ordered_greater_equal,
|
binary_expression_builder!(build_float_ordered_not_equal, FloatOrderedNotEqual);
|
||||||
BuildFloatOrderedGreaterEqual
|
|
||||||
);
|
|
||||||
binary_expression_builder!(build_float_ordered_less_than, BuildFloatOrderedLessThan);
|
|
||||||
binary_expression_builder!(build_float_ordered_less_equal, BuildFloatOrderedLessEqual);
|
|
||||||
binary_expression_builder!(build_float_ordered_equal, BuildFloatOrderedEqual);
|
|
||||||
binary_expression_builder!(build_float_ordered_not_equal, BuildFloatOrderedNotEqual);
|
|
||||||
|
|
||||||
binary_expression_builder!(build_float_unordered, BuildFloatUnordered);
|
binary_expression_builder!(build_float_unordered, FloatUnordered);
|
||||||
binary_expression_builder!(
|
binary_expression_builder!(
|
||||||
build_float_unordered_greater_than,
|
build_float_unordered_greater_than,
|
||||||
BuildFloatUnorderedGreaterThan
|
FloatUnorderedGreaterThan
|
||||||
);
|
);
|
||||||
binary_expression_builder!(
|
binary_expression_builder!(
|
||||||
build_float_unordered_greater_equal,
|
build_float_unordered_greater_equal,
|
||||||
BuildFloatUnorderedGreaterEqual
|
FloatUnorderedGreaterEqual
|
||||||
);
|
);
|
||||||
binary_expression_builder!(build_float_unordered_less_than, BuildFloatUnorderedLessThan);
|
binary_expression_builder!(build_float_unordered_less_than, FloatUnorderedLessThan);
|
||||||
binary_expression_builder!(
|
binary_expression_builder!(build_float_unordered_less_equal, FloatUnorderedLessEqual);
|
||||||
build_float_unordered_less_equal,
|
binary_expression_builder!(build_float_unordered_equal, FloatUnorderedEqual);
|
||||||
BuildFloatUnorderedLessEqual
|
binary_expression_builder!(build_float_unordered_not_equal, FloatUnorderedNotEqual);
|
||||||
);
|
|
||||||
binary_expression_builder!(build_float_unordered_equal, BuildFloatUnorderedEqual);
|
|
||||||
binary_expression_builder!(build_float_unordered_not_equal, BuildFloatUnorderedNotEqual);
|
|
||||||
|
|
||||||
binary_expression_builder!(build_fp_add, BuildFloatAdd);
|
binary_expression_builder!(build_fp_add, FloatAdd);
|
||||||
binary_expression_builder!(build_fp_sub, BuildFloatSub);
|
binary_expression_builder!(build_fp_sub, FloatSub);
|
||||||
binary_expression_builder!(build_fp_mul, BuildFloatMul);
|
binary_expression_builder!(build_fp_mul, FloatMul);
|
||||||
binary_expression_builder!(build_fp_div, BuildFloatDiv);
|
binary_expression_builder!(build_fp_div, FloatDiv);
|
||||||
binary_expression_builder!(build_fp_rem, BuildFloatRem);
|
binary_expression_builder!(build_fp_rem, FloatRem);
|
||||||
|
|
||||||
unary_expression_builder!(build_fp_abs, BuildFloatAbs);
|
unary_expression_builder!(build_fp_abs, FloatAbs);
|
||||||
|
|
||||||
unary_expression_builder!(build_not, BuildNot);
|
unary_expression_builder!(build_not, Not);
|
||||||
binary_expression_builder!(build_equal, BuildEqual);
|
binary_expression_builder!(build_equal, Equal);
|
||||||
binary_expression_builder!(build_not_equal, BuildNotEqual);
|
binary_expression_builder!(build_not_equal, NotEqual);
|
||||||
binary_expression_builder!(build_bool_and, BuildBoolAnd);
|
binary_expression_builder!(build_bool_and, BoolAnd);
|
||||||
binary_expression_builder!(build_bool_or, BuildBoolOr);
|
binary_expression_builder!(build_bool_or, BoolOr);
|
||||||
binary_expression_builder!(build_bool_xor, BuildBoolXor);
|
binary_expression_builder!(build_bool_xor, BoolXor);
|
||||||
|
|
||||||
expression_builder!(build_sext(op: RSymExpr, bits: u8) => BuildSext);
|
expression_builder!(build_sext(op: RSymExpr, bits: u8) => Sext);
|
||||||
expression_builder!(build_zext(op: RSymExpr, bits: u8) => BuildZext);
|
expression_builder!(build_zext(op: RSymExpr, bits: u8) => Zext);
|
||||||
expression_builder!(build_trunc(op: RSymExpr, bits: u8) => BuildTrunc);
|
expression_builder!(build_trunc(op: RSymExpr, bits: u8) => Trunc);
|
||||||
expression_builder!(build_int_to_float(op: RSymExpr, is_double: bool, is_signed: bool) => BuildIntToFloat);
|
expression_builder!(build_int_to_float(op: RSymExpr, is_double: bool, is_signed: bool) => IntToFloat);
|
||||||
expression_builder!(build_float_to_float(op: RSymExpr, to_double: bool) => BuildFloatToFloat);
|
expression_builder!(build_float_to_float(op: RSymExpr, to_double: bool) => FloatToFloat);
|
||||||
expression_builder!(build_bits_to_float(op: RSymExpr, to_double: bool) => BuildBitsToFloat);
|
expression_builder!(build_bits_to_float(op: RSymExpr, to_double: bool) => BitsToFloat);
|
||||||
expression_builder!(build_float_to_bits(op: RSymExpr) => BuildFloatToBits);
|
expression_builder!(build_float_to_bits(op: RSymExpr) => FloatToBits);
|
||||||
expression_builder!(build_float_to_signed_integer(op: RSymExpr, bits: u8) => BuildFloatToSignedInteger);
|
expression_builder!(build_float_to_signed_integer(op: RSymExpr, bits: u8) => FloatToSignedInteger);
|
||||||
expression_builder!(build_float_to_unsigned_integer(op: RSymExpr, bits: u8) => BuildFloatToUnsignedInteger);
|
expression_builder!(build_float_to_unsigned_integer(op: RSymExpr, bits: u8) => FloatToUnsignedInteger);
|
||||||
expression_builder!(build_bool_to_bits(op: RSymExpr, bits: u8) => BuildBoolToBits);
|
expression_builder!(build_bool_to_bits(op: RSymExpr, bits: u8) => BoolToBits);
|
||||||
|
|
||||||
binary_expression_builder!(concat_helper, ConcatHelper);
|
binary_expression_builder!(concat_helper, Concat);
|
||||||
expression_builder!(extract_helper(op: RSymExpr, first_bit:usize, last_bit:usize) => ExtractHelper);
|
expression_builder!(extract_helper(op: RSymExpr, first_bit:usize, last_bit:usize) => Extract);
|
||||||
|
|
||||||
fn notify_call(&mut self, _site_id: usize) {}
|
fn notify_call(&mut self, _site_id: usize) {}
|
||||||
|
|
||||||
@ -161,7 +156,7 @@ impl Runtime for TracingRuntime {
|
|||||||
}
|
}
|
||||||
|
|
||||||
fn push_path_constraint(&mut self, constraint: RSymExpr, taken: bool, site_id: usize) {
|
fn push_path_constraint(&mut self, constraint: RSymExpr, taken: bool, site_id: usize) {
|
||||||
self.write_message(SymExpr::PushPathConstraint {
|
self.write_message(SymExpr::PathConstraint {
|
||||||
constraint,
|
constraint,
|
||||||
taken,
|
taken,
|
||||||
site_id,
|
site_id,
|
||||||
@ -171,6 +166,9 @@ impl Runtime for TracingRuntime {
|
|||||||
|
|
||||||
impl Drop for TracingRuntime {
|
impl Drop for TracingRuntime {
|
||||||
fn drop(&mut self) {
|
fn drop(&mut self) {
|
||||||
self.writer.end().expect("failed to shut down writer");
|
// manually end the writer to update the length prefix
|
||||||
|
self.writer
|
||||||
|
.update_trace_header()
|
||||||
|
.expect("failed to shut down writer");
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
9
libafl_concolic/test/README.md
Normal file
9
libafl_concolic/test/README.md
Normal file
@ -0,0 +1,9 @@
|
|||||||
|
This folder contains all the code necessary to run a smoke test of the whole concolic tracing setup.
|
||||||
|
This is achieved by
|
||||||
|
1. Compiling SymCC. Dependencies are installed via `smoke_test_ubuntu_deps.sh`.
|
||||||
|
2. Compiling a custom runtime with tracing capability (`runtime_test`).
|
||||||
|
3. Compiling a test program using SymCC that instruments using the custom runtime.
|
||||||
|
4. Capturing an execution trace of the instrumented target using `dump_constraints` and a fixed input (`if_test_input`).
|
||||||
|
5. Snapshot-testing the captured trace against our expectation (`expected_constraints.txt`).
|
||||||
|
|
||||||
|
This whole process is orchestrated by `smoke_test.sh`.
|
@ -2,6 +2,7 @@
|
|||||||
name = "dump_constraints"
|
name = "dump_constraints"
|
||||||
version = "0.1.0"
|
version = "0.1.0"
|
||||||
edition = "2018"
|
edition = "2018"
|
||||||
|
authors = ["Julius Hohnerlein <julihoh@users.noreply.github.com>"]
|
||||||
|
|
||||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||||
|
|
||||||
|
@ -1,3 +1,7 @@
|
|||||||
|
//! This is a straight-forward command line utility that can dump constraints written by a tracing runtime.
|
||||||
|
//! It achieves this by running an instrumented target program with the necessary environment variables set.
|
||||||
|
//! When the program has finished executing, it dumps the traced constraints to a file.
|
||||||
|
|
||||||
use std::{
|
use std::{
|
||||||
ffi::OsString,
|
ffi::OsString,
|
||||||
fs::File,
|
fs::File,
|
||||||
@ -12,11 +16,8 @@ use structopt::StructOpt;
|
|||||||
use libafl::{
|
use libafl::{
|
||||||
bolts::shmem::{ShMem, ShMemProvider, StdShMemProvider},
|
bolts::shmem::{ShMem, ShMemProvider, StdShMemProvider},
|
||||||
observers::concolic::{
|
observers::concolic::{
|
||||||
serialization_format::{
|
serialization_format::{MessageFileReader, MessageFileWriter, DEFAULT_ENV_NAME},
|
||||||
shared_memory::DEFAULT_ENV_NAME, MessageFileReader, MessageFileWriter,
|
EXPRESSION_PRUNING, HITMAP_ENV_NAME, NO_FLOAT_ENV_NAME, SELECTIVE_SYMBOLICATION_ENV_NAME,
|
||||||
},
|
|
||||||
SymExpr, EXPRESSION_PRUNING, HITMAP_ENV_NAME, NO_FLOAT_ENV_NAME,
|
|
||||||
SELECTIVE_SYMBOLICATION_ENV_NAME,
|
|
||||||
},
|
},
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -113,7 +114,7 @@ fn main() {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// open a new scope to ensure our ressources get dropped before the exit call at the end
|
// open a new scope to ensure our resources get dropped before the exit call at the end
|
||||||
let output_file_path = opt.output.unwrap_or_else(|| "trace".into());
|
let output_file_path = opt.output.unwrap_or_else(|| "trace".into());
|
||||||
let mut output_file =
|
let mut output_file =
|
||||||
BufWriter::new(File::create(output_file_path).expect("unable to open output file"));
|
BufWriter::new(File::create(output_file_path).expect("unable to open output file"));
|
||||||
@ -140,9 +141,6 @@ fn main() {
|
|||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
writer
|
|
||||||
.write_message(SymExpr::End)
|
|
||||||
.expect("unable to write end message");
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1,30 +1,30 @@
|
|||||||
1 GetInputByte { offset: 0 }
|
1 InputByte { offset: 0 }
|
||||||
2 GetInputByte { offset: 1 }
|
2 InputByte { offset: 1 }
|
||||||
3 GetInputByte { offset: 2 }
|
3 InputByte { offset: 2 }
|
||||||
4 GetInputByte { offset: 3 }
|
4 InputByte { offset: 3 }
|
||||||
5 ConcatHelper { a: 2, b: 1 }
|
5 Concat { a: 2, b: 1 }
|
||||||
6 ConcatHelper { a: 3, b: 5 }
|
6 Concat { a: 3, b: 5 }
|
||||||
7 ConcatHelper { a: 4, b: 6 }
|
7 Concat { a: 4, b: 6 }
|
||||||
8 ConcatHelper { a: 2, b: 1 }
|
8 Concat { a: 2, b: 1 }
|
||||||
9 ConcatHelper { a: 3, b: 8 }
|
9 Concat { a: 3, b: 8 }
|
||||||
10 ConcatHelper { a: 4, b: 9 }
|
10 Concat { a: 4, b: 9 }
|
||||||
11 ExtractHelper { op: 10, first_bit: 7, last_bit: 0 }
|
11 Extract { op: 10, first_bit: 7, last_bit: 0 }
|
||||||
12 ExtractHelper { op: 10, first_bit: 15, last_bit: 8 }
|
12 Extract { op: 10, first_bit: 15, last_bit: 8 }
|
||||||
13 ExtractHelper { op: 10, first_bit: 23, last_bit: 16 }
|
13 Extract { op: 10, first_bit: 23, last_bit: 16 }
|
||||||
14 ExtractHelper { op: 10, first_bit: 31, last_bit: 24 }
|
14 Extract { op: 10, first_bit: 31, last_bit: 24 }
|
||||||
15 ConcatHelper { a: 12, b: 11 }
|
15 Concat { a: 12, b: 11 }
|
||||||
16 ConcatHelper { a: 13, b: 15 }
|
16 Concat { a: 13, b: 15 }
|
||||||
17 ConcatHelper { a: 14, b: 16 }
|
17 Concat { a: 14, b: 16 }
|
||||||
18 BuildInteger { value: 2, bits: 32 }
|
18 Integer { value: 2, bits: 32 }
|
||||||
19 BuildMul { a: 18, b: 17 }
|
19 Mul { a: 18, b: 17 }
|
||||||
20 BuildInteger { value: 7, bits: 32 }
|
20 Integer { value: 7, bits: 32 }
|
||||||
21 BuildSignedLessThan { a: 19, b: 20 }
|
21 SignedLessThan { a: 19, b: 20 }
|
||||||
22 PushPathConstraint { constraint: 21, taken: false, site_id: 11229456 }
|
22 PathConstraint { constraint: 21, taken: false, site_id: 11229456 }
|
||||||
22 ConcatHelper { a: 12, b: 11 }
|
22 Concat { a: 12, b: 11 }
|
||||||
23 ConcatHelper { a: 13, b: 22 }
|
23 Concat { a: 13, b: 22 }
|
||||||
24 ConcatHelper { a: 14, b: 23 }
|
24 Concat { a: 14, b: 23 }
|
||||||
25 BuildInteger { value: 7, bits: 32 }
|
25 Integer { value: 7, bits: 32 }
|
||||||
26 BuildSignedRem { a: 24, b: 25 }
|
26 SignedRem { a: 24, b: 25 }
|
||||||
27 BuildInteger { value: 0, bits: 32 }
|
27 Integer { value: 0, bits: 32 }
|
||||||
28 BuildNotEqual { a: 26, b: 27 }
|
28 NotEqual { a: 26, b: 27 }
|
||||||
29 PushPathConstraint { constraint: 28, taken: true, site_id: 11122032 }
|
29 PathConstraint { constraint: 28, taken: true, site_id: 11122032 }
|
||||||
|
@ -2,6 +2,7 @@
|
|||||||
name = "runtime_test"
|
name = "runtime_test"
|
||||||
version = "0.1.0"
|
version = "0.1.0"
|
||||||
edition = "2018"
|
edition = "2018"
|
||||||
|
authors = ["Julius Hohnerlein <julihoh@users.noreply.github.com>"]
|
||||||
|
|
||||||
[lib]
|
[lib]
|
||||||
crate-type = ["cdylib"]
|
crate-type = ["cdylib"]
|
||||||
|
@ -1,3 +1,5 @@
|
|||||||
|
//! Just a small runtime to be used in the smoke test.
|
||||||
|
|
||||||
use symcc_runtime::{
|
use symcc_runtime::{
|
||||||
export_runtime,
|
export_runtime,
|
||||||
filter::NoFloat,
|
filter::NoFloat,
|
||||||
|
Loading…
x
Reference in New Issue
Block a user