Symbolic Execution Checker

The symbolic-execution checker is exposed through the lotus-check symex subcommand and is backed by the top-level SymbolicExecution subsystem.

Engine Location: lib/SymbolicExecution/

Headers: include/SymbolicExecution/

Tool Frontend: tools/checker/lotus-check-symex.cpp

Overview

The engine performs path-sensitive symbolic execution over the guarded value-flow graph. It tracks symbolic scalar values, access paths, guarded memory facts, taint-derived facts, and path conditions, then uses SMT-backed feasibility checks before emitting bug reports.

The main build target is CanarySymbolicExecution. The target remains separate from lib/Analysis because the subsystem owns a full driver, symbolic state model, solver bridge, memory modeling layer, taint model, and LLVM pass wrapper.

Core Components

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

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

  • ProgramVar and Property* – Name symbolic values and represent scalar properties such as offsets, sizes, and affine expressions.

  • ConstraintRepr and PathCondSolver – Encode symbolic predicates and discharge path-feasibility queries.

  • MemoryAPI and GVFGUtility – Connect symbolic execution to allocation modeling, data layout, library summaries, and GVFG construction.

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

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

Usage

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

Tests

Focused unit tests live under tests/unit/SymbolicExecution and build against CanarySymbolicExecution.

See Also