IKOS Analyzer and API Specification Tools ========================================= Lotus bundles the full IKOS analyzer and API-spec pipeline from the IKOS API-spec fork. The pipeline discovers external functions in LLVM 14 bitcode, scaffolds C stubs from IR declarations, generates candidate bodies through an LLM endpoint, and compiles and links stubs with signature verification. Enable and install ------------------ The full integration is optional. It uses Python 3.8+, LLVM/Clang 14, Boost (filesystem and thread), GMP/GMPXX, TBB, and SQLite3. Enable and build it with:: cmake -S . -B build -DLOTUS_ENABLE_IKOS=ON cmake --build build --target lotus-ikos -j4 build/bin/lotus-ikos example.c build/bin/ikos-report output.db ``LOTUS_ENABLE_IKOS`` also enables the API-spec commands. The native targets are ``ikos-analyzer``, ``ikos-pp``, and ``ikos-import``. Reusable libraries are ``CanaryIKOSCore``, ``CanaryIKOSAR``, ``CanaryIKOSFrontend``, and ``CanaryIKOSPreprocessor``. They build inside Lotus using C++17; no separate IKOS checkout, Python virtual environment, or build-time package downloads are required. Optional APRON domains can be enabled with ``-DLOTUS_IKOS_ENABLE_APRON=ON`` when APRON and its dependencies are installed. For only the Python pipeline, without building the analyzer:: cmake -S . -B build -DLOTUS_ENABLE_IKOS_API_SPEC=ON build/bin/lotus-ikos-stub --help build/bin/lotus-ikos-api-census --help build/bin/lotus-ikos-api-spec --help If the LLVM installation used by Lotus lacks clang, specify a complete LLVM 14 tool directory with ``-DLOTUS_IKOS_LLVM_BIN=/path/to/llvm-14/bin``. To install the full IKOS component, including the pipeline:: cmake --install build --component ikos --prefix /desired/prefix Use ``--component ikos-api-spec`` to install only the pipeline. Compatibility commands ``ikos``, ``ikos-report``, ``ikos-view``, ``ikos-config``, ``ikos-scan``, ``ikos-scan-cc``, ``ikos-scan-c++``, ``ikos-scan-extract``, ``ikos-stub``, and ``ikos-api-census`` accompany a full installation. The installed commands use a private payload under ``share/lotus/ikos-api-spec``. They do not require the original Downloads directory or a system Python ``ikos`` package. Analysis and the pipeline use the Python standard library; syntax highlighting in the web viewer optionally uses Pygments. ``LOTUS_IKOS_LLVM_BIN`` overrides the configured tool path at runtime. VS Code and clangd ------------------ Enable IKOS in the build used by the editor, then refresh its scoped index:: cmake -S . -B build -DLOTUS_ENABLE_IKOS=ON cmake --build build --target ikos-index The ``ikos-index`` target does not compile the analyzer. It extracts IKOS's actual compilation records into ``build/ikos-index/compile_commands.json`` and links that database under ``third-party/ikos-api-spec`` for clangd discovery. This prevents standalone IKOS headers from inheriting unrelated Lotus compile commands. Rerun the target after changing build options or dependency paths. For the rest of Lotus, use ``build/compile_commands.json``. If keeping a database in the repository root, use a symlink instead of an outdated copy:: ln -sfn build/compile_commands.json compile_commands.json After changing the database, run ``clangd: Restart language server`` from VS Code's command palette. The generated databases are local, ignored files and are excluded from installation. Offline workflow ---------------- Compile the program with clang 14, then inspect and scaffold missing functions:: clang-14 -g -O0 -emit-llvm -c example.c -o example.bc lotus-ikos-api-census ir /path/to/directory-containing-bitcode lotus-ikos-stub check example.bc lotus-ikos-stub scaffold -o stubs example.bc Implement the generated bodies and remove their placeholder markers before linking:: lotus-ikos-stub link --stub-dir stubs --fail-missing -o example.stubbed.bc example.bc lotus-ikos example.stubbed.bc The linker rejects unfinished placeholders and mismatched signatures by default. Already validated database entries can be reused without an LLM call:: lotus-ikos-api-spec prefetch -o stubs --db-dir /path/to/stubdb example.bc Generation and validation ------------------------- Generation uses an explicitly configured provider or compatible endpoint:: lotus-ikos-api-spec generate -o stubs --provider deepseek --model MODEL example.bc Set the provider's key in its documented environment variable, such as ``DEEPSEEK_API_KEY`` or ``OPENAI_API_KEY``. Provider model presets come from the imported snapshot; use ``--model`` to select a model available to your account. No model calls occur during configuration, installation, or the Lotus tests. Default generation requires Linux and Bubblewrap for native differential execution. IKOS self-checks and abstract-domain judging automatically use the bundled analyzer in a full build. For a pipeline-only installation, supply the matching fork via ``IKOS_PREFIX`` or ``ikos`` on PATH. An ordinary upstream IKOS release may not implement the fork's extended memory intrinsics. Census, scaffolding, compilation, linking, and database lookup work without that analyzer on macOS as well as Linux. Missing sandbox support does not cause an automatic fallback to unsandboxed execution. Analyzer self-checks work on macOS, where the judge omits the unsupported ``RLIMIT_AS`` memory cap while retaining analyzer and subprocess timeouts. Failed analyzer processes or missing/corrupt result databases provide no self-check evidence. Semantic scope -------------- The builtin classification table describes IKOS models, not the models of every Lotus analysis. Generated stubs use ``__ikos_*`` intrinsics, which the bundled IKOS analyzer implements, including the fork's memory extensions. Other LLVM bitcode consumers must understand those intrinsics to interpret their assumptions, nondeterminism, and memory effects. This integration does not add those semantics to other Lotus checker engines. Use ``--force-stub`` to override IKOS builtin classification when preparing a particular function manually. Differential tests provide evidence over sampled inputs; they do not establish soundness for every input. Review generated assumptions for the intended analysis. Tests and provenance -------------------- With ``LOTUS_BUILD_TESTS=ON`` and the ``verification`` test subsystem selected:: ctest --test-dir build -R '^ikos_' --output-on-failure The suite includes the imported regressions and an offline workflow exercising the actual Lotus commands, successful bitcode linking, placeholder rejection, signature mismatch rejection, and empty-database prefetch. Full-build tests also prove intrinsic assumptions, detect division by zero, verify that linked-stub constraints reach callers, and exercise reporting and compiler wrappers. Tests requiring unavailable Linux tools, IKOS, or upstream experiment fixtures report skips. Source provenance and local modifications are recorded in ``third-party/ikos-api-spec/README.lotus.md``. The imported code retains its NASA Open Source Agreement 1.3 license and copyright notices.