Instrumentation Passes

Lotus provides several LLVM instrumentation passes for preparing programs for verification.

Available Passes

BreakCritLoops

Breaks critical loops for better slicing and control dependence analysis.

Usage:

lotus-opt input.bc -break-crit-loops -o output.bc

What it does:

  • Identifies basic blocks that jump back to themselves via critical edges

  • Splits these blocks to improve control dependence computation

  • Useful before running PDG-based slicing

DeleteUndefined

Deletes calls to undefined functions and replaces non-void undefined functions with nondeterministic values.

Usage:

lotus-opt input.bc -delete-undefined -o output.bc

What it does:

  • Removes calls to undefined void functions

  • Replaces undefined non-void functions with verifier.nondet.undef.* calls

  • Preserves calls to verifier functions and standard library functions

  • Useful for preparing programs with missing function definitions

InitializeUninitialized

Initializes stack-allocated variables with nondeterministic values.

Usage:

lotus-opt input.bc -init-uninit -o output.bc

What it does:

  • Finds all alloca instructions in function entry blocks

  • Replaces uninitialized uses with calls to verifier.nondet.init.* functions

  • Useful for verification where uninitialized variables should be treated as nondeterministic

MakeNondet

Replaces selected input functions with nondeterministic value generators.

Usage:

lotus-opt input.bc -make-nondet -o output.bc

Configuration:

The pass accepts a comma-separated list of function names to replace:

lotus-opt input.bc -make-nondet \
  --make-nondet-targets=rand,getchar,fgetc,scanf \
  -o output.bc

What it does:

  • Replaces calls to specified functions (e.g., rand(), getchar()) with nondeterministic values

  • Preserves return type semantics

  • Useful for abstracting away I/O and random number generation

PrepareOverflows

Instruments signed arithmetic operations with explicit overflow checks.

Usage:

lotus-opt input.bc -prep-overflows -o output.bc

What it does:

  • Finds signed integer arithmetic operations (add, sub, mul)

  • Replaces them with overflow-checking intrinsics (llvm.sadd.with.overflow, etc.)

  • Calls __VERIFIER_error() if overflow detected

  • Useful for overflow property checking

Example Workflow

A typical verification workflow:

# 1. Initialize uninitialized variables
lotus-opt input.bc -init-uninit -o step1.bc

# 2. Replace I/O with nondet
lotus-opt step1.bc -make-nondet -o step2.bc

# 3. Instrument overflow checks
lotus-opt step2.bc -prep-overflows -o prepared.bc

# 4. Verify
lotus-verify prepared.bc --property overflow --backend clam --run

All Passes Together

You can enable all instrumentation passes at once:

lotus-opt input.bc -init-uninit -make-nondet -prep-overflows -o output.bc

Or use the convenience flag (if available):

lotus-opt input.bc -ip-all -o output.bc

Integration with Verification

These passes are designed to work with Lotus’s verification backends:

  • InitializeUninitialized: Prepares programs for abstract interpretation (CLAM)

  • MakeNondet: Essential for symbolic execution (SeaHorn, Sifa)

  • PrepareOverflows: Required for overflow property checking

See Verification Backend Abstraction for more information on using these with verification tools.