sfu-rsl · momvart · Jul 20, 2026 · Jul 20, 2026 · Jul 20, 2026 · Jul 20, 2026
diff --git a/README.md b/README.md
@@ -1,54 +1,51 @@
 # Leaf
 
-Concolic execution for Rust through MIR instrumentation.
-
-
-## Table of Contents
-- [Getting Started](#getting-started)
-- [Documentation](#documentation)
-
-## Getting Started
-1. Clone the repository.
-1. Install `leafc` using
-    ```
-    cargo install --path ./compiler
-    ```
-1. Compile target programs using `leafc`, e.g.,
-    ```
-    leafc samples/hello_world.rs
-    ```
-1. Enable logging for Leaf's backend using `LEAF_LOG` environment variable.
-    ```
-    export LEAF_LOG="info"
-    ```
-1. Run the compiled program.
-    ```
-    hello_world
-    ```
-1. An output similar to the following is expected from the execution.
-    ```log
-    2024-12-10 00:40:55  INFO leafrt Initializing runtime library
-    2024-12-10 00:40:55  INFO leafrt::pri::basic::instance Initializing basic backend
-    2024-12-10 00:40:55  INFO leafrt::backends::basic::outgen Setting up binary output writing to directory: output
-    2024-12-10 00:40:55  INFO leafrt::pri::basic::instance Basic backend initialized
-    2024-12-10 00:40:55  INFO leafrt::backends::basic::sym_vars Added a new symbolic variable: <Var1: u8> = 10u8
-    2024-12-10 00:40:55  INFO leafrt::trace::log Notified about constraint {!(<(<Var1: u8>, 5u8))} at step Def(0:5)[2]
-    2024-12-10 00:40:55  INFO leafrt::outgen Found a solution:
-    {
-        "1": 0u8,
-    }
-    ```
-
-This was a demonstration of the basic workflow to perform dynamic symbolic execution using Leaf.
-
-Leaf comes with a compiler (`leafc`) that instruments programs.
-It is a wrapper around the Rust compiler and should be usable in any existing command
-in place of `rustc`.
-The instrumented program calls the backend during runtime, providing the information about the events inside the program
-including the constraints on the variables for the path currently being taken.
-By marking a variables of interest as symbolic, the system records the constraints on them, and later provides output
-based on them, e.g., concrete values for them which cause the program take paths different from the current one.
-For further information please refer to documentations.
+Leaf is a Rust-oriented framework for dynamic analysis built around MIR instrumentation. It wraps the Rust compiler through `leafc`, instruments a program at compile time, and routes runtime events to pluggable backends for tracing, symbolic execution, and related analyses.
+
+## Project layout
+
+- `compiler/`: the `leafc` driver and instrumentation pipeline
+- `runtime/lib`: the shared abstraction library for implementing runtime backends
+- `runtime/backends/`: concrete backend implementations
+- `common/`: shared facilities and definitions used across the project
+
+## Requirements
+
+- Rustup and cargo to install nightly toolchains, `rustc` libraries and building the project.
+- Python for helper scripts (e.g., toolchain builder) in the repository
+
+## Quick start
+1. Clone the repository and build the compiler:
+   ```console
+   $ git clone https://github.com/sfu-rsl/leaf.git
+   $ cd leaf
+   $ cargo install --path ./compiler
+   ```
+
+1. Build a runtime backend, for example the control-flow tracer:
+   ```console
+   $ cargo build -p runtime_cf_tracer
+   ```
+
+1. Make the shared library discoverable to the generated program:
+   ```console
+   $ mkdir -p target/debug/runtime_cf_tracer
+   $ ln -sf target/debug/runtime_cf_tracer.so target/debug/runtime_cf_tracer/libleafrt.so
+   $ export LD_LIBRARY_PATH="$PWD/target/debug/runtime_cf_tracer:$LD_LIBRARY_PATH"
+   ```
+
+1. Compile a sample program with `leafc`:
+   ```console
+   $ leafc samples/hello_world.rs
+   ```
+
+1. Run the instrumented binary with logging enabled:
+   ```console
+   $ export LEAF_LOG="info"
+   $ ./hello_world
+   ```
+
+The generated program will emit runtime events through the active backend, which can be inspected through the logging output or any backend-specific artifacts.
 
 ## Documentation
 
@@ -57,17 +54,8 @@ Further information, tutorials, and technical details are collected in Leaf Book
 
 ## License
 
-Licensed under either of
-
- * Apache License, Version 2.0
-   ([LICENSE-APACHE](LICENSE-APACHE) or http://www.apache.org/licenses/LICENSE-2.0)
- * MIT license
-   ([LICENSE-MIT](LICENSE-MIT) or http://opensource.org/licenses/MIT)
-
-at your option.
+Leaf is licensed under the MIT or Apache-2.0 licenses.
 
-## Contribution
+- Apache License, Version 2.0: [LICENSE-APACHE](LICENSE-APACHE)
+- MIT License: [LICENSE-MIT](LICENSE-MIT)
 
-Unless you explicitly state otherwise, any contribution intentionally submitted
-for inclusion in the work by you, as defined in the Apache-2.0 license, shall be
-dual licensed as above, without any additional terms or conditions.
diff --git a/common/Cargo.toml b/common/Cargo.toml
@@ -1,5 +1,6 @@
 [package]
 name = "common"
+license = { workspace = true }
 version = { workspace = true }
 edition = "2021"
 
@@ -69,5 +70,5 @@ z3-sys = { workspace = true, optional = true }
 unexpected_cfgs = { level = "warn", check-cfg = [
     'cfg(core_build)',
     'cfg(info_db_fmt, values("json", "rkyv"))',
-    'cfg(refs_inlining)'
+    'cfg(refs_inlining)',
 ] }
diff --git a/compiler/Cargo.toml b/compiler/Cargo.toml
@@ -1,5 +1,6 @@
 [package]
 name = "compiler"
+license = { workspace = true }
 version = { workspace = true }
 edition = "2024"
 

diff --git a/docs/src/leaf.md b/docs/src/leaf.md
@@ -2,7 +2,6 @@
 Concolic execution for Rust through MIR instrumentation.
 
 Welcome to project Leaf, a tool to perform dynamic symbolic execution for Rust programs.
-Leaf helps you with tracking the constraints put on particular variables of interest during the execution of the program.
 
 Leaf aims to be robust, extensible, and easily-integrable within real world Rust testing stacks.
 

diff --git a/docs/src/user_guide/getting_started.md b/docs/src/user_guide/getting_started.md
@@ -1,91 +1,91 @@
 # Getting Started
-Although currently working with the first releases of Leaf, we aim to provide a rather straightforward workflow for the users.
 
-Please follow the instruction below to try Leaf in your environment.
+Leaf is a Rust-oriented framework for dynamic analysis built around MIR instrumentation. The workflow is:
 
-## Installing Leaf
+1. compile and instrument a target program with `leafc`, and
+1. provide a runtime backend that receives callbacks from the instrumented program,
+4. run the instrumented program with the backend plugged in.
+
+## Requirements
 
-### Requirements
-- Rust (`rustup`)
+- Rust
 - Python
+- A working C toolchain and linker
 
-You can install Leaf using `cargo` and by building the source code.
-
-1. Clone the repository.
-    ```console
-    $ git clone https://github.com/sfu-rsl/leaf.git
-    $ cd leaf
-    ```
-1. Install Leaf's compiler named as `leafc` using
-    ```console
-    $ cargo install --path ./compiler
-    ```
-## Performing Concolic Execution
-As an instrumentation-based dynamic analyzer, Leaf instruments programs such that
-they expose information about their behavior during each execution.
-Therefore, concolic execution is achieved by compiling the target program and
-running the executable.
-
-1. Pick a program you want to do concolic execution for. Some are available in `samples` directory of the source tree.
-    ```rust
-    fn main() {
-        let x: u8 = 10;
-        if x < 5 {
-            println!("Hello, world!");
-        }
-    }
-    ```
-
-1. Mark a variable interest as symbolic.
-    ```rust
-    // samples/hello_world.rs
-
-    use leaf::annotations::*;
-    fn main() {
-        let x: u8 = 10.mark_symbolic();
-        if x < 5 {
-            println!("Hello, world!");
-        }
-    }
-    ```
-
-1. Compile your target program using `leafc` as you would do with `rustc`. (The first compilation takes longer, bear with it!)
-    ```console
-    $ leafc ./hello_world.rs
-    ```
-
-1. Prepare the environment to observe the execution through the standard error
-   by setting `LEAF_LOG` variable. e.g.,
-    ```bash
-    export LEAF_LOG="info"
-    ```
-1. Execute the compiled program.
-    ```console
-    $ ./hello_world 
-    ```
-1. An output similar to the following is expected from the execution.
-    ```log
-    2024-12-10 00:40:55  INFO leafrt Initializing runtime library
-    2024-12-10 00:40:55  INFO leafrt::pri::basic::instance Initializing basic backend
-    2024-12-10 00:40:55  INFO leafrt::backends::basic::outgen Setting up binary output writing to directory: output
-    2024-12-10 00:40:55  INFO leafrt::pri::basic::instance Basic backend initialized
-    2024-12-10 00:40:55  INFO leafrt::backends::basic::sym_vars Added a new symbolic variable: <Var1: u8> = 10u8
-    2024-12-10 00:40:55  INFO leafrt::trace::log Notified about constraint {!(<(<Var1: u8>, 5u8))} at step Def(0:5)[2]
-    2024-12-10 00:40:55  INFO leafrt::outgen Found a solution:
-    {
-        "1": 0u8,
+## Installing Leaf
+
+1. Clone the repository and enter the workspace.
+   ```console
+   $ git clone https://github.com/sfu-rsl/leaf.git
+   $ cd leaf
+   ```
+
+1. Install the compiler frontend.
+   ```console
+   $ cargo install --path ./compiler
+   ```
+
+## Preparing Dynamic Analysis
+
+1. Build a runtime backend, for example symbolic execution.
+   ```console
+   $ cargo build -p runtime_symex
+   ```
+
+1. Make the runtime shared library discoverable to the instrumented binary.
+   ```console
+   $ mkdir -p target/debug/runtime_symex
+   $ ln -sf "$(find target/debug -maxdepth 1 -name 'libleafrt*.so' | head -n 1)" target/debug/runtime_symex/libleafrt.so
+   $ export LD_LIBRARY_PATH="$PWD/target/debug/runtime_symex:$LD_LIBRARY_PATH"
+   ```
+
+## Analyzing a Program
+
+Leaf ships with sample programs under the `samples/` directory. A minimal example is the `hello_world` sample.
+```rust
+fn main() {
+    let x: u8 = core::hint::black_box(10);
+    #[cfg(leafc)]
+    let x: u8 = {
+        use leaf::annotations::*;
+        x.mark_symbolic()
+    };
+
+    if x < 5 {
+        println!("Hello, world!");
     }
-    ```
-    The logs include information about the constraints put on the variables marked as symbolic for the path taken in the execution.
+}
+```
 
-1. Given the current default configuration, a folder named `leaf_out` also gets generated
-   which contains alternative values for the symbolic variables that should cause
-   the execution take other paths than the one taken, which we call diverging inputs.
+1. Compile the sample with `leafc`.
    ```console
-   $ ls ./leaf_out
-   0.bin
+   $ leafc samples/hello_world.rs
    ```
 
------------
+2. Enable logging for the runtime.
+   ```console
+   $ export LEAF_LOG="info"
+   ```
+
+3. Run the generated binary.
+   ```console
+   $ ./hello_world
+   ```
+
+You should see runtime events emitted by the active backend. The exact output depends on the chosen backend and logging configuration, but the execution should complete and produce instrumentation traces or analysis data. With the example symbolic execution backend in effect, an output similar to the following is expected.
+```log
+2024-12-10 00:40:55  INFO leafrt Initializing runtime library
+2024-12-10 00:40:55  INFO leafrt::pri::basic::instance Initializing basic backend
+2024-12-10 00:40:55  INFO leafrt::backends::basic::outgen Setting up binary output writing to directory: output
+2024-12-10 00:40:55  INFO leafrt::pri::basic::instance Basic backend initialized
+2024-12-10 00:40:55  INFO leafrt::backends::basic::sym_vars Added a new symbolic variable: <Var1: u8> = 10u8
+2024-12-10 00:40:55  INFO leafrt::trace::log Notified about constraint {!(<(<Var1: u8>, 5u8))} at step Def(0:5)[2]
+2024-12-10 00:40:55  INFO leafrt::outgen Found a solution:
+{
+    "1": 0u8,
+}
+```
+
+## Next steps
 
-More details about each step is provided in the rest of the book.
+The rest of the book covers the compiler pipeline, runtime backends, and more advanced analysis workflows in greater detail.
diff --git a/docs/src/user_guide/recipes/cargo.md b/docs/src/user_guide/recipes/cargo.md
@@ -11,3 +11,7 @@ $ export RUSTC=leafc
 $ cargo build
 ```
 
+## Leaf's Modifications
+
+`leafc` is slightly specialized when used by cargo for compiling crate's dependencies.
+(TODO)
diff --git a/docs/src/user_guide/recipes/div_input.md b/docs/src/user_guide/recipes/div_input.md
@@ -1,5 +1,8 @@
 # Diverging Input Generation
 
+> [!IMPORTANT]
+> This document is currently obsolete and will be removed with further developments of the book. The orchestrators mentioned in this tutorial are currently moved out of the project.
+
 Each instance of concolic execution of a program, records a trace of the constraints put on symbolic variables at each
 step of the execution.
 Conditional branches are the major source of these constraints and whether they are held or not

diff --git a/docs/src/user_guide/recipes/fuzzing.md b/docs/src/user_guide/recipes/fuzzing.md
@@ -1,5 +1,8 @@
 # Fuzzing
 
+> [!IMPORTANT]
+> This document is currently obsolete and will be removed with further developments of the book. The orchestrators mentioned in this tutorial are currently moved out of the project.
+
 One of the use cases of concolic execution, which is demonstrated to be effective,
 is hybrid fuzzing, in which fuzzing is aided with solver-found inputs generated by symbolic
 execution to take certain paths inside the program that other techniques are inefficient

diff --git a/macros/Cargo.toml b/macros/Cargo.toml
@@ -1,5 +1,6 @@
 [package]
 name = "macros"
+license = { workspace = true }
 version = { workspace = true }
 edition = "2021"
 

diff --git a/runtime/backends/cf_tracer/Cargo.toml b/runtime/backends/cf_tracer/Cargo.toml
@@ -1,5 +1,6 @@
 [package]
 name = "runtime_backend_cf_tracer"
+license = { workspace = true }
 version = { workspace = true }
 edition = "2021"
 

diff --git a/runtime/backends/mdsan/Cargo.toml b/runtime/backends/mdsan/Cargo.toml
@@ -1,5 +1,6 @@
 [package]
 name = "runtime_backend_mdsan"
+license = { workspace = true }
 version = { workspace = true }
 edition = "2021"
 

diff --git a/runtime/backends/symex/Cargo.toml b/runtime/backends/symex/Cargo.toml
@@ -1,5 +1,6 @@
 [package]
 name = "runtime_backend_symex"
+license = { workspace = true }
 version = { workspace = true }
 edition = "2021"
 

diff --git a/runtime/flavors/cf_tracer/Cargo.toml b/runtime/flavors/cf_tracer/Cargo.toml
@@ -1,5 +1,6 @@
 [package]
 name = "runtime_cf_tracer"
+license = { workspace = true }
 version = { workspace = true }
 edition = "2021"
 

diff --git a/runtime/flavors/mdsan/Cargo.toml b/runtime/flavors/mdsan/Cargo.toml
@@ -1,5 +1,6 @@
 [package]
 name = "runtime_mdsan"
+license = { workspace = true }
 version = { workspace = true }
 edition = "2021"
 

diff --git a/runtime/flavors/noop/Cargo.toml b/runtime/flavors/noop/Cargo.toml
@@ -1,5 +1,6 @@
 [package]
 name = "runtime_noop"
+license = { workspace = true }
 version = { workspace = true }
 edition = "2021"