Checker Tools

This page summarizes the bug-finding tools under tools/checker/. For a feature-oriented overview and examples, see Bug Detection with Lotus.

lotus-kint – Integer and Array Bug Finder

A static bug finder for integer-related and taint-style bugs (originally from OSDI 12).

Binary: lotus-kint Location: tools/checker/lotus_kint.cpp

Usage:

./build/bin/lotus-kint [options] <input IR file>

Bug Checker Options:

  • -check-all – Enable all checkers (overrides individual settings)

  • -check-int-overflow – Enable integer overflow checker

  • -check-div-by-zero – Enable division by zero checker

  • -check-bad-shift – Enable bad shift checker

  • -check-array-oob – Enable array index out of bounds checker

  • -check-dead-branch – Enable dead branch checker

Performance Options:

  • -function-timeout=<seconds> – Maximum time to spend analyzing a single function (0 = no limit, default: 10)

Logging Options:

  • -log-level=<level> – Set logging level (debug, info, warning, error, none, default: info)

  • -quiet – Suppress most log output

  • -log-to-stderr – Redirect logs to stderr instead of stdout

  • -log-to-file=<filename> – Redirect logs to the specified file

Detects:

The tool detects various integer-related bugs:

  1. Integer overflow: Detects potential integer overflow in arithmetic operations

  2. Division by zero: Detects potential division by zero errors

  3. Bad shift: Detects invalid shift amounts

  4. Array out of bounds: Detects potential array index out of bounds access

  5. Dead branch: Detects impossible branches in conditional statements

Examples:

# Enable all checkers
./build/bin/lotus-kint -check-all input.ll

# Enable specific checkers
./build/bin/lotus-kint -check-int-overflow -check-div-by-zero input.ll

# Set function timeout and log level
./build/bin/lotus-kint -function-timeout=30 -log-level=debug input.ll

# Quiet mode with output to file
./build/bin/lotus-kint -quiet -log-to-file=analysis.log input.ll

lotus-ae – Abstract Execution Bug Checker

Abstract-execution-based bug detection for memory-safety issues.

Binary: lotus-ae Location: tools/checker/lotus-ae.cpp

Usage:

./build/bin/lotus-ae --all input.bc
./build/bin/lotus-ae --overflow --null-deref input.bc

Key options:

  • --all

  • --overflow, --null-deref, --use-after-free, --invalid-free, --mem-leak

  • --handle-recur=top|widen-only|widen-narrow

  • --widen-delay=<N>

lotus-taint – Taint Analysis

IFDS-based interprocedural taint analysis tool.

Binary: lotus-taint Location: tools/checker/lotus_taint.cpp

Detects:

  • Flows from untrusted sources (e.g., input) to sensitive sinks (e.g., system calls)

  • Optional reaching-definitions analysis mode

Usage:

./build/bin/lotus-taint [options] input.bc

Key options:

  • -analysis=0 – Taint analysis (default)

  • -analysis=1 – Reaching-definitions analysis

  • -sources=<f1,f2,...> – Custom source functions

  • -sinks=<f1,f2,...> – Custom sink functions

  • -max-results=<N> – Limit number of detailed flows

  • -verbose – Detailed path information

For end-to-end examples (command injection, SQL injection, etc.), see Bug Detection with Lotus and IFDS / IDE Engine.

lotus-concur – Concurrency Bug Checker

Static analysis for shared-memory concurrency bugs plus dedicated OpenMP and MPI checks.

Binary: lotus-concur Location: tools/checker/lotus_concur.cpp

Detects:

  • Data races on shared variables

  • Locking discipline violations

  • Potential deadlocks (lock ordering issues)

  • OpenMP taskgroup/atomic-region mismatches and partial task synchronization

  • MPI request lifecycle bugs, collective mismatches, simple MPI deadlocks, and RMA issues

Usage:

./build/bin/lotus-concur [options] input.bc

Key options:

  • --checks=race,deadlock,atomicity,condvar,lock-mismatch,openmp,mpi – enable only the listed checks

  • --check-openmp – run dedicated OpenMP checks

  • --check-mpi – run dedicated MPI checks

  • --analysis-only – dump analysis facts without bug emission

Typical workflow:

  1. Compile multi-threaded C/C++ program to LLVM bitcode

  2. Run lotus-concur on the bitcode

  3. Inspect reported shared variables and threads involved in races

Detailed concurrency examples and recommended patterns are in Bug Detection with Lotus.

lotus-saber – Source-Sink Resource Checker

Saber-based bug detection over sparse value-flow graphs.

Binary: lotus-saber Location: tools/checker/lotus-saber.cpp

Usage:

./build/bin/lotus-saber input.bc
./build/bin/lotus-saber --all input.bc
./build/bin/lotus-saber --double-free --file input.bc