Abstract Execution Checker

The AE subsystem provides abstract-execution-based bug detection.

Headers: include/Checker/AE/

Implementation: lib/Checker/AE/

Tool: lotus-ae in tools/checker/lotus-ae.cpp

Overview

AE runs abstract interpretation and specialized detectors to report memory safety issues such as buffer overflows, null dereferences, use-after-free, and invalid frees.

Main components

  • AbstractInterpretation drives the fixpoint analysis.

  • AEDetector and its concrete detectors implement bug-specific checks.

  • Value abstractions such as AbstractValue, NumericValue, and AbstractState model execution state during analysis.

  • RelationSolver and related utilities support symbolic reasoning in the abstract domain.

Checks supported

  • Buffer overflow

  • Null pointer dereference

  • Use-after-free

  • Invalid free

  • Memory leak

Command-line usage

./build/bin/lotus-ae --all input.bc
./build/bin/lotus-ae --overflow --null-deref input.bc
./build/bin/lotus-ae --handle-recur=widen-narrow --widen-delay=5 input.bc

Important options

  • --all enables all AE bug detectors.

  • --overflow, --null-deref, --use-after-free, --invalid-free, and --mem-leak enable individual checks.

  • --handle-recur chooses the recursion strategy.

  • --widen-delay delays widening in loops.

  • -v prints more detailed traces for findings.

See also