SymCC Concolic Tracing Runtime Rust Bindings

This crate allows you to build custom runtimes for SymCC. See the documentation for details.

lib.rs:

SymCC Runtime Bindings

This crate contains bindings to the SymCC runtime interface to be used from Rust. A SymCC runtime can be used with either SymCC or 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:

[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"