crabllvm (seahorn/crab-llvm) is incompatible with LLVM 16 — `--add-invariants` is a no-op

[GuilhermeBn198]

Summary

The --add-invariants flag (which adds program invariants via Crab-LLVM) is a no-op in the current build because the Crab-LLVM binary is never built.

Root cause

• cmake/FindCrabLlvm.cmake uses ExternalProject_Add to pull seahorn/crab-llvm, but this module is never included by the modern CMakeLists.txt (LLVM 16 / New PM era).
• seahorn/crab-llvm is a legacy SeaHorn dependency tied to LLVM 6–12 and is not compatible with LLVM 16.
• modules/frontend/caller.cpp compileToCrabLlvm() invokes ${MAP2CHECK_PATH}/bin/crabllvm/bin/crabllvm.py, which does not exist in any produced install layout.

Current workaround (landed)

modules/frontend/map2check.cpp now detects the absence of bin/crabllvm/bin/crabllvm.py and falls back to plain compilation with a warning, instead of breaking the pipeline (fix: fall back to plain compile when crabllvm is not built).

Desired outcome (future)

Either:

1. Build crab-llvm against LLVM 16 (if upstream supports it), wiring FindCrabLlvm.cmake into the modern build and installing the binary so --add-invariants works again; or
2. Drop the feature: remove --add-invariants, compileToCrabLlvm(), and FindCrabLlvm.cmake from the codebase, and update the docs (docs/map2check_migration_plan.md mentions Crab-LLVM as "presente mas não ativo").

Context

--add-invariants was used as a pass-2 fallback in the CASTLE/Juliet baseline evaluation; it is currently skipped because of this gap. Related: modules/frontend/caller.cpp compileToCrabLlvm().

[github-actions]

Welcome to the Map2Check! We are excited that this is your first issue!

[GuilhermeBn198]

The landed fallback never fires for the project's own usage

Running the CASTLE/Juliet baseline surfaced a gap in the workaround described above. The fallback warning is real, but it is unreachable for bitcode input — and both evaluation harnesses feed pre-compiled .bc.

modules/frontend/map2check.cpp:226 guards the entire branch:

if (!is_llvmir_in) {
    if (args.invCrabLlvm) {
      ...
      Map2Check::Log::Warning("crabllvm is not built — ignoring --add-invariants");

When the input is already LLVM IR, is_llvmir_in is true, the block is skipped, and --add-invariants is accepted and dropped with no diagnostic at all.

Reproduction

$ clang-16 -c -emit-llvm -g -O0 x.c -o x.bc

$ map2check --memtrack --add-invariants --timeout 20 x.bc
  (no mention of crabllvm or invariants)

$ map2check --memtrack --add-invariants --timeout 20 x.c
  crabllvm is not built — ignoring --add-invariants

Measured cost

tests/castle/run_castle_evaluation.sh uses --add-invariants as a pass-2 fallback whenever pass 1 returns UNKNOWN. Because the flag is inert, that second pass is bit-for-bit identical to the first. In the v5 baseline (217 CASTLE cases, 2026-08-16):

• 12 cases triggered pass 2, consuming 481 s
• not one verdict changed — every case kept its pass-1 result
• the CSV's invariants column reports yes for all 12, so the recorded data claims a technique that was never applied

Grepping all 217 retained raw outputs for the warning returns 0 matches, which is how this went unnoticed.

Suggested scope adjustment

Independently of which of the two outcomes above is chosen (build crab-llvm against LLVM 16, or drop the feature), two smaller fixes are worth landing now because they are cheap and stop the silent data corruption:

1. Move the availability check outside the !is_llvmir_in guard so the warning reaches every caller that passed the flag. Invariant generation itself still only applies to a source compile — it is only the diagnostic that needs to escape the guard. A second warning for the IR case (input is already LLVM IR — ignoring --add-invariants) makes the distinction explicit.
2. Gate the CASTLE pass-2 fallback behind an opt-in env var while this issue is open, so the harness stops paying for a pass that cannot change its own outcome.

Happy to open a PR for both if that is useful.

[GuilhermeBn198]

Resolved — --add-invariants works again, on Clam

Closing this as option 1 from the original issue: build the invariant generator against LLVM 16 and wire it in. Landed across #56, #57 and #58, all merged to develop.

What the investigation found

seahorn/crab-llvm was not abandoned — it was renamed to seahorn/clam. Same project, same API metadata; branch dev16 pins CLAM_LLVM_VERSION 16, which is exactly this image's LLVM. So there was a supported path all along, under a name nothing in the repo referenced. Written up in docs/reports/2026-08-16-crabllvm-review.md, which also compares the alternatives that were considered and rejected (IKOS, the bare Crab library, llvm.assume, slicing).

What shipped

Clam is built into the dev image (Dockerfile.dev §7b) and installed to /opt/clam. --add-invariants is gated behind -DENABLE_CLAM=ON and the driver actually being present at $CLAM_DIR/bin/clam.py. It stays opt-in on purpose: an unsound invariant yields a wrong TRUE, not an error, which is the worst possible failure mode for a verifier.

The silent no-op is gone. The workaround described in this issue — fall back to plain compilation with a warning — was itself part of the problem: it is how the flag stayed dead through an entire baseline evaluation without anyone noticing. Map2Check now refuses with exit code 3 and names the flag, the missing generator, and the fix. The guard also moved into main(), because main() discarded the return value of map2check_execution(), and out of the if (!is_llvmir_in) branch, which is why .bc input accepted and ignored the flag while .c input did not.

Two defects that would have made a working build produce nothing:

1. The legacy flag list injected zero invariants. Measured, not assumed: the baseline invocation yields 5 verifier.assume calls; adding --crab-promote-assume drops it to 1 (it rewrites verifier.assume into the llvm.assume intrinsic, which NonDetPass does not match), and adding --llvm-pp-loops drops it to 0. Both were in the old crab-llvm invocation. Had crab-llvm been revived with its original flags, it would have injected nothing and still reported success.
2. The image build never compiled. Clam's sea-dsa defines seadsa::mkTLIGetter with a redundant namespace qualification inside its own namespace: clang reports -Wextra-qualification, GCC 11 rejects it outright. The Clam RUN was picking up GCC because ENV CC=clang-16 is declared 88 lines below it. Fixed in fix(docker): build Clam with clang-16, and validate Dockerfile.dev on PRs #58, which also makes the publish workflow run on PRs touching Dockerfile.dev so an unbuildable image can never reach develop again.

How it is kept honest

• Dockerfile.dev fails the image build if a probe program yields zero injected verifier.assume calls. Confirmed in the fix(docker): build Clam with clang-16, and validate Dockerfile.dev on PRs #58 build log: Clam injects invariants: OK.
• CI job Invariants (Clam) (tests/integration/test_add_invariants.sh) asserts both contracts from one file and prints CAPABILITY: ABSENT|PRESENT, so the transition is visible in the job log rather than inferred.
• The three callers (utils/map2check-wrapper.py, utils/map2check-wrapper-reg-test.py, the CASTLE harness) deliberately kept passing --add-invariants while it was broken. Removing the flag to silence the failure is what would restore the silence this work exists to remove.
• utils/build_crabllvm.py is deleted.

Remaining

Dockerfile.dev clones clam and its dependencies from moving dev branches. Being pinned to SHAs in a follow-up — tracked separately, not a blocker for this issue.