Symbolic Execution

This section documents the top-level symbolic execution engine that backs the lotus-check symex checker and other path-sensitive analyses.

Headers: include/SymbolicExecution/

Implementation: lib/SymbolicExecution/

Build target: CanarySymbolicExecution

Tool frontend: lotus-check symex (see Symbolic Execution Checker)

Overview

The SymbolicExecution subsystem is a standalone, path-sensitive symbolic execution engine. It operates over the guarded value-flow graph (GVFG), tracks symbolic scalar values and memory facts along feasible paths, and uses SMT-backed path-condition checks before emitting bug reports.

The subsystem lives at the top level of the source tree (lib/SymbolicExecution/ and include/SymbolicExecution/) rather than under lib/Analysis/ because it owns a full driver, symbolic state model, solver bridge, memory modeling layer, taint model, and LLVM pass wrapper. It is consumed by the checker framework through SymbolicExecutionWrapper.

Core Components

The engine is composed of the following headers under include/SymbolicExecution/:

Driver and state

  • AnalysisDriver – Coordinates whole-module symbolic execution and summary scheduling across functions.

  • AnalysisState – Represents symbolic memory, guarded values, points-to items, interprocedural summaries, taint updates, and pending bug queries.

  • AnalysisLimit – Configurable resource and depth budgets that bound exploration.

Symbolic values and properties

  • ProgramVar – Names symbolic values tied to LLVM values and contexts.

  • PropertyAllocator – Allocates and manages symbolic properties.

  • PropertyValue, PropertyInteger, PropertySym – Represent scalar properties such as offsets, sizes, and affine expressions attached to symbolic values.

  • BigInteger – Arbitrary-precision integer support for symbolic reasoning.

Path conditions and solving

  • ConstraintRepr – Encodes symbolic predicates used in path conditions.

  • PathCondSolver – Discharges path-feasibility queries through the SMT (Z3) backend; paths proven infeasible are pruned before reporting.

Memory and control flow

  • MemoryAPI – Connects symbolic execution to allocation modeling, data layout, and library function summaries.

  • GVFGUtility – Builds and queries the guarded value-flow graph that the engine walks.

  • InstResolver – Resolves instruction-level targets (call targets, memory locations) during exploration.

  • DomTreePass – Dominator-tree reasoning used for reachability and join handling.

Taint and reporting

  • TaintModel – Provides source, transfer, and sink facts used by taint-sensitive bug checks.

  • SymbolicExecutionWrapper – Integrates the engine with the LLVM pass pipeline and the checker report infrastructure (BugReportMgr).

Analysis flow

A typical symbolic-execution run proceeds as follows:

  1. GVFG construction – GVFGUtility builds the guarded value-flow graph, capturing data and guarded control dependencies.

  2. Driver scheduling – AnalysisDriver selects entry functions and schedules interprocedural exploration, applying summaries where available.

  3. Path exploration – AnalysisState advances along paths, updating symbolic memory, properties, and taint facts.

  4. Feasibility check – PathCondSolver queries the SMT solver; paths whose path conditions are unsatisfiable are pruned.

  5. Bug query – At suspect instructions (e.g. dereferences, divisions), the engine emits bug queries through AnalysisState.

  6. Reporting – Confirmed bugs flow through SymbolicExecutionWrapper into the centralized BugReportMgr (JSON/SARIF output).

Usage

The engine is invoked through the unified checker frontend:

./build/bin/lotus-check symex input.bc
./build/bin/lotus-check symex input.bc --symex-checkers=null-deref,uaf

For the full list of subcommand options, see Symbolic Execution Checker.

Programmatic usage

The engine is exposed as an LLVM pass via SymbolicExecutionWrapper and can be added to a pass pipeline like other Lotus passes:

#include "SymbolicExecution/SymbolicExecutionWrapper.h"

// Within a pass manager setup:
auto *seWrapper = new SymbolicExecutionWrapperPass();
pm.add(seWrapper);

Tests

Focused unit tests live under tests/unit/SymbolicExecution and build against CanarySymbolicExecution. They cover spec compatibility and the taint model.

See Also