Checker Tooling

Subcommand registration and entry points for the lotus-check unified checker frontend.

Header: include/Checker/Framework/Subcommands.h

Implementation: tools/checker/

Build target: lotus-check

Overview

The Checker Tooling module provides the subcommand infrastructure for the unified lotus-check binary. Each checker category registers an llvm::cl::SubCommand with a descriptive name and help text, enabling dispatch from a single entry point.

Note

These subcommands are an internal C++ option-registration mechanism. The public command-line interface selects an engine with --engine=<name> (e.g. lotus-check --engine=kint input.bc); the old lotus-check kint input.bc subcommand form is rejected.

Checker Subcommands

File: Subcommands.h

Declares accessor functions for each subcommand (defined in lib/Checker/Framework/Subcommands.cpp):

#include "Checker/Framework/Subcommands.h"

auto &sub = lotus::checker::tooling::genericSubCommand();
auto &sub = lotus::checker::tooling::kintSubCommand();
auto &sub = lotus::checker::tooling::taintSubCommand();
auto &sub = lotus::checker::tooling::concurrencySubCommand();
auto &sub = lotus::checker::tooling::pulseSubCommand();
auto &sub = lotus::checker::tooling::fitxSubCommand();
auto &sub = lotus::checker::tooling::saberSubCommand();
auto &sub = lotus::checker::tooling::aeSubCommand();
auto &sub = lotus::checker::tooling::symexSubCommand();

Registered Subcommands

Subcommand	Engine selected via `--engine=<name>`
`generic`	Run declarative and registry-backed checks
`kint`	Run the KINT integer checker
`taint`	Run the IFDS-based taint analysis
`concur`	Run the concurrency checker suite
`pulse`	Run the Pulse checker
`fitx`	Run the FiTx checker suite
`saber`	Run the Saber checker
`ae`	Run the abstract-execution checker
`symex`	Run the symbolic-execution checker

Usage

./build/bin/lotus-check --engine=kint input.bc --checks=all
./build/bin/lotus-check --engine=concur input.bc --checks=data-race

Parameter namespaces

Options with one cross-engine contract remain global, for example --checks, --log-level, --analysis-stats, and the shared reporting options. Parameters whose semantics belong to an engine use the qualified form --<engine>.<parameter>. For example, KINT summary behavior is configured by --kint.summary-mode, while Pulse path solving is configured by --pulse.smt. No unqualified compatibility aliases are provided.

Use lotus-check --list-parameters to print all global and engine groups, or lotus-check --engine=<name> --help for one engine.