Troubleshooting and FAQ

This document helps resolve common issues and answers frequently asked questions.

Installation Issues

LLVM Version Mismatch

Problem: CMake can’t find LLVM or finds wrong version.

CMake Error: Could not find LLVM
-- or --
Found LLVM 15.0.0 but need 14.0.0

Solution:

Check that LLVM 14.x is installed and visible on PATH:

llvm-config --version

If multiple LLVM versions are installed, point CMake to the desired one explicitly:

cmake ../ -DLLVM_BUILD_PATH=/path/to/llvm-14/lib/cmake/llvm

Z3 Not Found

Problem: Z3 library or headers not found during build.

Could not find Z3 libraries
fatal error: z3.h: No such file or directory

Solution:

Install Z3 development package:

# Ubuntu/Debian
sudo apt-get install libz3-dev

# macOS
brew install z3

# Or build from source
git clone https://github.com/Z3Prover/z3
cd z3
python scripts/mk_make.py
cd build && make && sudo make install

Specify Z3 path:

cmake ../ -DZ3_ROOT=/path/to/z3/install

Boost Not Found

Problem: Boost libraries required for SeaHorn, CLAM, and/or CclyzerAA not found.

Could NOT find Boost

Solution:

Install Boost:

# Ubuntu/Debian
sudo apt-get install libboost-all-dev

# macOS
brew install boost

Or specify custom Boost:

cmake ../ -DCUSTOM_BOOST_ROOT=/path/to/boost

Lotus can auto-download Boost:

cmake ../ -DAUTO_DOWNLOAD_BOOST=ON

Compilation Errors

Problem: Undefined reference errors during linking.

undefined reference to `llvm::PassRegistry::registerPass'

Solution:

Ensure LLVM was built with:

cmake -DLLVM_ENABLE_RTTI=ON -DLLVM_ENABLE_EH=ON ../llvm

Clean and rebuild:

cd build
rm -rf *
cmake ../
make -j$(nproc)

Analysis Issues

Analysis Crashes

Problem: Tool crashes with segmentation fault.

Segmentation fault (core dumped)

Solution:

Run with debug build:

cmake ../ -DCMAKE_BUILD_TYPE=Debug
make
gdb --args ./bin/tool input.bc
(gdb) run
(gdb) backtrace

Check input validity:

opt -verify input.bc -o /dev/null

Common causes:
- Malformed LLVM IR
- Null pointer dereference in analysis
- Stack overflow (increase limit: ulimit -s unlimited)

Analysis Takes Too Long

Problem: Analysis runs indefinitely or for hours.

Solution:

Use faster analysis mode:

# For alias analysis, use context-insensitive
./bin/aser-aa -analysis-mode=ci input.bc

# For CLAM, use interval domain
./bin/clam --crab-dom=int input.bc

Set timeout:

timeout 300 ./bin/tool input.bc  # 5 minutes

For Kint, set function timeout:

./bin/lotus-kint -function-timeout=30 input.ll

Reduce precision:

# Disable field sensitivity
./bin/aser-aa -field-sensitive=false input.bc

# Limit context depth
./bin/aser-aa -analysis-mode=1-cfa -max-context-depth=2 input.bc

Out of Memory

Problem: Analysis exhausts system memory.

std::bad_alloc
Killed

Solution:

Increase available memory (if possible)
Use more scalable analysis:

./bin/dyck-aa input.bc

Analyze incrementally:

# Split module into parts
llvm-extract -func=main input.bc -o main.bc
./bin/tool main.bc

Limit analysis scope:

# Intraprocedural only
./bin/clam --crab-inter=false input.bc

False Positives

Problem: Analysis reports bugs that don’t exist.

Solution:

Use more precise analysis:

# 1-CFA instead of CI
./bin/aser-aa -analysis-mode=1-cfa input.bc

# Zones domain instead of intervals
./bin/clam --crab-dom=zones input.bc

Validate with dynamic analysis:

./bin/dynaa-instrument input.bc -o inst.bc
clang inst.bc libRuntime.a -o inst
LOG_DIR=logs ./inst
./bin/dynaa-check input.bc logs/pts.log basic-aa

Add annotations to code:

void my_function(int *p) {
    __builtin_assume(p != NULL);  // Help analysis
    *p = 10;
}

Missing Bugs (False Negatives)

Problem: Analysis doesn’t detect known bugs.

Solution:

Enable all checkers:

./bin/lotus-kint -check-all input.ll

Use more comprehensive analysis:

# Interprocedural
./bin/clam --crab-inter --crab-check=all input.bc

# Context-sensitive taint
./bin/lotus-taint -analysis=0 -verbose input.bc

Check if bug type is supported:

./bin/lotus-kint --help  # See supported checks

Tool-Specific Issues

CLAM Issues

Problem: CLAM fails with “unsupported instruction”.

Unsupported LLVM instruction: <instruction>

Solution:

Preprocess bitcode:

./bin/clam-pp --crab-lower-unsigned-icmp \
               --crab-lower-select \
               input.bc -o prep.bc
./bin/clam prep.bc

Use suitable domain:

# Some domains don't support all operations
./bin/clam --crab-dom=int input.bc  # Basic support

Problem: CLAM reports “Could not allocate memory”.

Solution:

Use less expensive domain:

# Polyhedra is expensive
./bin/clam --crab-dom=zones input.bc  # Use zones instead

Disable tracking:

./bin/clam --crab-track=num input.bc  # Track only numbers

DyckAA Issues

Problem: DyckAA produces too many alias pairs.

Solution:

Enable function type checking:

# Don't use -no-function-type-check

The analysis is very precise but conservative. This is expected behavior.

Problem: Call graph is incomplete.

Solution:

# Ensure indirect calls are analyzed
./bin/dyck-aa -dot-dyck-callgraph input.bc

PDG Query Issues

Problem: PDG query returns empty set unexpectedly.

Solution:

Check node names:

# Function names are case-sensitive
MATCH (n:FUNC_ENTRY) WHERE n.name = 'Main' RETURN n  # Wrong
MATCH (n:FUNC_ENTRY) WHERE n.name = 'main' RETURN n  # Correct

Verify PDG was built:

./bin/pdg-query -q "MATCH (n) RETURN n" input.bc  # Should show nodes

Use verbose mode:

./bin/pdg-query -v -q "MATCH (n) RETURN n" input.bc

Problem: Query parser error.

Solution:

Check query syntax:

# Wrong
MATCH (n:FUNC_ENTRY) WHERE n.name = main RETURN n

# Correct
MATCH (n:FUNC_ENTRY) WHERE n.name = 'main' RETURN n

Use interactive mode to test:

./bin/pdg-query -i input.bc
> MATCH (n:FUNC_ENTRY) WHERE n.name = 'main' RETURN n

Taint Analysis Issues

Problem: No taint flows detected but vulnerability exists.

Solution:

Specify custom sources/sinks:

./bin/lotus-taint -sources="my_input_func" \
                   -sinks="my_output_func" \
                   input.bc

Check that source and sink functions are actually called
Use lotus-taint for interprocedural flow:

./bin/lotus-taint input.bc

Performance Tuning

Speeding Up Analysis

Choose appropriate analysis
Reduce scope:

# Analyze specific function
llvm-extract -func=main input.bc -o main.bc
./bin/tool main.bc

Use preprocessing:

# Simplify IR first
opt -mem2reg -simplifycfg input.bc -o simplified.bc
./bin/tool simplified.bc

Parallel analysis (if tool supports):

Reducing Memory Usage

Use sparse representations:

# Field-insensitive uses less memory
./bin/aser-aa -field-sensitive=false input.bc

Limit analysis depth:

./bin/aser-aa -analysis-mode=1-cfa input.bc  # Not 2-cfa

Process in batches:

# Analyze files separately
for f in *.bc; do
    ./bin/tool "$f"
done

Frequently Asked Questions

General Questions

Q: Which alias analysis should I use?

A: Depends on your needs

Q: Can Lotus analyze C++ code?

A: Yes! Compile to LLVM IR:

clang++ -emit-llvm -c code.cpp -o code.bc
./bin/tool code.bc

Q: Does Lotus support multi-threaded programs?

A: Yes, use:

lotus-concur for concurrency bugs
aser-aa -analysis-mode=origin for thread-aware analysis
MHP analysis in concurrency module

Q: How do I visualize results?

A: Generate DOT files:

# Call graph
./bin/dyck-aa -dot-dyck-callgraph input.bc

# PDG
./bin/pdg-query -dump-dot input.bc

# Sea-DSA memory graph
./bin/seadsa-tool --sea-dsa-dot --outdir=output/ input.bc

# Convert to PDF
dot -Tpdf output.dot -o output.pdf

Q: Can I integrate Lotus into my own tool?

A: Yes! See API Reference for programmatic usage.

Analysis Questions

Q: What’s the difference between flow-sensitive and flow-insensitive?

A:

Flow-insensitive: Single points-to set per variable for entire program. Faster but less precise.
Flow-sensitive: Different points-to sets at different program points. Slower but more precise.

Example:

int x, y;
int *p;
p = &x;  // p points to x
p = &y;  // p points to y

// Flow-insensitive: p may point to {x, y} everywhere
// Flow-sensitive: p points to {x} at line 4, {y} at line 5

Q: What’s context sensitivity?

A: Distinguishing different calling contexts:

void foo(int *p) { *p = 10; }

int main() {
    int x, y;
    foo(&x);  // Context 1
    foo(&y);  // Context 2
}

Context-insensitive: Analyzes foo once, p may point to {x, y}
Context-sensitive: Analyzes foo twice, p points to {x} in context 1, {y} in context 2

Q: How accurate is the analysis?

A: Lotus analyses are sound (no false negatives for most analyses) but may have false positives. Trade-off between precision and performance.

Q: Can I customize source/sink definitions?

A: Yes:

./bin/lotus-taint -sources="my_source1,my_source2" \
                   -sinks="my_sink1,my_sink2" \
                   input.bc

Or create custom analysis (see Developer Guide).

CLAM Questions

Q: Which abstract domain should I use?

A:

Intervals (int): Fast, simple ranges [l, u]
Zones (zones): Moderate, difference constraints (x - y ≤ c)
Octagons (oct): More precise, diagonal constraints (±x ± y ≤ c)
Polyhedra (pk): Most precise, but expensive

Start with zones as good balance.

Q: What’s interprocedural analysis?

A: Analyzes across function boundaries:

# Intraprocedural: each function separately
./bin/clam input.bc

# Interprocedural: considers call context
./bin/clam --crab-inter input.bc

Interprocedural is more precise but slower.

Q: Can CLAM verify my assertions?

A: Yes:

int main() {
    int x = 5;
    assert(x >= 0 && x <= 10);  // CLAM can verify this
    return 0;
}

./bin/clam --crab-check=assert input.bc

Bug Detection Questions

Q: Why does Kint report false positives?

A: Kint uses range analysis which may be imprecise. Use more precise domain or add assertions to help analysis:

void process(int x) {
    if (x < 0 || x > 100) return;
    // Now Kint knows 0 <= x <= 100
    int y = x + 50;  // No overflow warning
}

Q: How do I reduce false positives?

A:

Use preprocessing:

./bin/clam-pp --crab-lower-unsigned-icmp input.bc -o prep.bc

Use more precise analysis
Add annotations/assertions
Validate with dynamic analysis (DynAA)

Q: Can I output results in JSON/SARIF?

A: Yes:

# CLAM JSON output
./bin/clam -ojson=results.json input.bc

# Kint with SARIF (via BugReportMgr)
./bin/lotus-kint -check-all -output-sarif=results.sarif input.ll

Compilation Questions

Q: How do I compile multi-file projects?

A:

# Compile each file
clang -emit-llvm -c file1.c -o file1.bc
clang -emit-llvm -c file2.c -o file2.bc

# Link into single module
llvm-link file1.bc file2.bc -o program.bc

# Analyze
./bin/tool program.bc

Q: Should I use .bc or .ll files?

A:

.bc: Binary format, faster to load, smaller
.ll: Text format, human-readable, easier to debug

Both work with Lotus. Use .bc for production, .ll for debugging.

Q: What optimization level should I use?

A:

# For analysis, usually no optimization or -O1
clang -emit-llvm -c -O0 code.c -o code.bc  # No optimization
clang -emit-llvm -c -O1 code.c -o code.bc  # Light optimization

# Higher optimization may complicate analysis
clang -emit-llvm -c -O3 code.c -o code.bc  # Not recommended

Common Error Messages

“Module verification failed”

Error:

Module verification failed: <details>

Solution: Your LLVM IR is malformed. Verify with:

opt -verify input.bc -o /dev/null

Fix the IR or recompile from source.

“Pass ‘X’ is not initialized”

Error:

Pass 'X' is not initialized

Solution: Initialize pass registry:

initializeCore(*PassRegistry::getPassRegistry());

“Couldn’t find alias information”

Error: Pass expects alias analysis but none provided.

Solution: Add alias analysis to pass manager:

PM.add(createBasicAAWrapperPass());
PM.add(myPass);

“Out of range access” or “Vector index out of bounds”

Error: Accessing invalid array/vector index.

Solution: This is usually a bug in the analysis. Report it with:

# Minimal reproducible example
clang -emit-llvm -c minimal.c -o minimal.bc
./bin/tool minimal.bc

Getting Help

Documentation

index - Main documentation
Architecture Overview - Framework architecture
API Reference - API documentation
Tutorials and Examples - Usage examples
Developer Guide - Extending Lotus

Support Channels

GitHub Issues: https://github.com/ZJU-PL/lotus/issues
- Bug reports
- Feature requests
- Help with errors
GitHub Discussions: https://github.com/ZJU-PL/lotus/discussions
- General questions
- Best practices
- Show and tell
Stack Overflow: Tag questions with [lotus-analysis] and [llvm]

Reporting Bugs

When reporting bugs, include:

Lotus version: git rev-parse HEAD
LLVM version: llvm-config --version
System: OS, compiler version
Input file: Minimal reproducible example
Command: Exact command that fails
Output: Full error message
Backtrace: If crashed, GDB backtrace

Example bug report:

**Description**: DyckAA crashes on input file

**Environment**:
- Lotus: commit abc123def
- LLVM: 14.0.0
- OS: Ubuntu 22.04
- GCC: 11.3.0

**To Reproduce**:
1. Compile: clang -emit-llvm -c test.c -o test.bc
2. Run: ./bin/dyck-aa test.bc

**Error**:
Segmentation fault (core dumped)

**Backtrace**:
#0 DyckGraph::addEdge (this=0x0, ...)
...

**Input file**: [attach test.c]

Contributing

See Developer Guide for how to contribute code, documentation, or tests.

Troubleshooting and FAQ

Installation Issues

LLVM Version Mismatch

Z3 Not Found

Boost Not Found

Compilation Errors

Analysis Issues

Analysis Crashes

Analysis Takes Too Long

Out of Memory

False Positives

Missing Bugs (False Negatives)

Tool-Specific Issues

CLAM Issues

DyckAA Issues

PDG Query Issues

Taint Analysis Issues

Performance Tuning

Speeding Up Analysis

Reducing Memory Usage

Frequently Asked Questions

General Questions

Analysis Questions

CLAM Questions

Bug Detection Questions

Compilation Questions

Common Error Messages

“Module verification failed”

“Pass ‘X’ is not initialized”

“Couldn’t find alias information”

“Out of range access” or “Vector index out of bounds”

Getting Help

Documentation

Support Channels

Reporting Bugs

Contributing

See Also