Symbolic Execution

The top-level symbolic execution engine in Lotus backs the lotus-check --engine=symex checker and other path-sensitive analyses.

Headers: include/SymbolicExecution/

Implementation: lib/SymbolicExecution/

Build target: CanarySymbolicExecution

Tool frontend: lotus-check --engine=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.

Directory layout

Headers and implementations are grouped by architectural responsibility:

  • Core/ – the symbolic execution engine and its fundamental state/value abstractions (driver, AnalysisState, AnalysisSummary, symbolic memory, guarded value sets, CStringState, taint state, scalar properties).

  • Solver/ – constraint representation and solver infrastructure (ConstraintRepr, PathCondSolver, SummarySolverManager).

  • Checks/ – query representation and bug-specific checking logic (the query hierarchy and the per-bug query construction, inlining, and reporting).

  • Integration/ – adapters to LLVM/Lotus/GVFG infrastructure (SymbolicExecutionWrapper, GVFGUtility).

Core does not depend on Checks; Checks may inspect Core state and use Solver functionality, and Integration sits at the outer boundary.

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.

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 --engine=symex input.bc
./build/bin/lotus-check --engine=symex input.bc --checks=null-deref,use-after-free

For the full list of engine 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/Integration/SymbolicExecutionWrapper.h"

// Within a pass manager setup:
auto *seWrapper = new llvm::SymbolicExecutionWrapper();
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