Pulse Checker

Pulse is Lotus’s witness-oriented bug finder. It is inspired by Infer Pulse and uses biabductive analysis with incorrectness-logic semantics: it under- approximates program behavior to report bugs that should correspond to a feasible execution, rather than trying to prove all executions safe.

Library Location: lib/Checker/Pulse/

Headers: include/Checker/Pulse/

Tool Location: tools/checker/lotus_pulse.cpp

Build Target: lotus-pulse

Overview

Pulse combines several ideas:

  • Incorrectness logic: favor witnessable bugs over whole-program safety proofs.

  • Biabduction: track both the current post-state and the missing preconditions required to make a witness feasible.

  • Path sensitivity: keep separate states for feasible branches, subject to a bounded disjunct limit.

  • Interprocedural summaries: summarize callees as pre/post pairs and materialize inferred preconditions at call sites.

At a high level the checker performs bounded symbolic execution over LLVM IR, records concrete error traces, and flushes deduplicated diagnostics through the shared BugReportMgr backend.

Core Representation

PulseChecker coordinates the analysis:

  • Builds an SCC-aware function schedule for summary construction

  • Traverses CFGs with bounded disjunction and loop abstraction

  • Dispatches instructions to transfer functions and library models

  • Converts detected issues into diagnostics and bug reports

The core abstract state is AbductiveDomain:

  • Post-state: heap, stack, address attributes, taint, and path facts along the current witness path

  • Pre-state: facts that had to be abduced to justify a later dereference or access

  • Path formula: equalities, nullness facts, disequalities, and arithmetic constraints used to prune infeasible paths

Runtime progress is represented by ExecutionDomain:

  • ContinueProgram for normal symbolic execution

  • Stopped variants such as ExitProgram, AbortProgram, and latent abort states when the checker needs caller context before turning an issue into a report

Key Components

The Pulse tree is organized by responsibility:

  • Checker/: main checker driver, instruction semantics, and summary wiring

  • Core/: formulas, call state, substitution, memory model, and value history

  • Domain/: abductive state, joins, disjunctive and non-disjunctive domains, loop abstraction, taint, and operations

  • Interproc/: summaries, specialization, transitive info, and library models

  • Report/: diagnostics, latent issue handling, logging, and report flushing

Not every concept has a dedicated .cpp file. For example, PulseMemory, PulseValueHistory, and PulseInvalidation are currently header-defined types used by the implementation rather than standalone translation units.

Detected Bug Classes

Pulse currently registers and reports these issue types:

  • Use After Free

  • Null Pointer Dereference

  • Uninitialized Read

  • Taint Error

  • Out Of Bounds Access

  • Invalid Free

  • Stack Variable Address Escape

  • Unnecessary Copy

The checker also tracks Const-Refable Parameter information, but that path is not yet emitted as a first-class PulseDiagnostic.

Interprocedural Behavior

Pulse summarizes functions as disjunctive pre/post pairs:

  • Each summary entry records an inferred precondition, a post-state, path formulas, an optional return value, and optional latent issue information.

  • Call-site application materializes the callee’s inferred precondition into the caller state.

  • Calls inside the current SCC are treated conservatively while summaries are still unstable.

  • Unknown or rejected summaries are tracked so the caller can fall back to a conservative unknown-result path instead of fabricating a witness.

Loops and Path Explosion

Pulse is intentionally bounded:

  • kMaxDisjuncts = 10 limits how many disjunctive states are retained

  • kMaxCallDepth = 5 limits recursive interprocedural exploration

  • LoopAbstraction applies widening and path-stamp based convergence checks

  • --no-smt disables SMT-backed path pruning for a faster, less precise mode

These limits trade recall for scalability. In practice, they can introduce false negatives by pruning or merging feasible witnesses too aggressively.

Command-Line Usage

Basic usage:

./build/bin/lotus-pulse input.bc

Common options:

  • -v: enable verbose logging

  • --log-level=<level>: none, error, warning, info, debug, or trace

  • --pulse-stats[=true|false]: print Pulse statistics

  • --json-output=<path>: emit the shared JSON report format

  • --min-score=<0-100>: filter exported reports by confidence

  • --no-smt: disable SMT solving when checking path feasibility

Example:

./build/bin/lotus-pulse --log-level=debug --json-output=report.json input.bc

Programmatic Usage

#include "Alias/AliasAnalysisWrapper/AliasAnalysisWrapper.h"
#include "Checker/Pulse/Checker/PulseChecker.h"
#include "Checker/Report/BugReportMgr.h"

auto AA = std::make_unique<lotus::AliasAnalysisWrapper>(
    *M, lotus::AAConfig::UnderApprox());

pulse::PulseChecker checker(M.get(), AA.get());
checker.analyze();

BugReportMgr &mgr = BugReportMgr::get_instance();
mgr.deduplicate_reports(true);
mgr.print_summary(llvm::outs());

Testing

The main unit tests live in:

  • tests/unit/Checker/Pulse/PulseCheckerTest.cpp for end-to-end checker behavior and reporting

  • tests/unit/Pulse/PulseFormulaTest.cpp for formula-level reasoning

Run the relevant tests from the build directory with:

ctest --output-on-failure -R 'pulse_checker_test|PulseFormulaTest'

Limitations

Pulse is designed to avoid non-witnessable reports on the behaviors it models, but precision still depends on the quality of its summaries, path reasoning, and library models.

Current practical limitations include:

  • bounded disjunction and call depth

  • incomplete library modeling

  • summary rejection when caller facts do not satisfy a callee witness

  • loss of precision in complex loops and merged control flow

See Also