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

Activity

1. github-actions commented on Aug 13, 2026

   

   github-actionsBot

   on Aug 13, 2026 – with GitHub Actions

   More actions

   Welcome to the Map2Check! We are excited that this is your first issue!
2. GuilhermeBn198 commented on Aug 16, 2026

   

   GuilhermeBn198

   on Aug 16, 2026

   CollaboratorAuthor

   More actions

   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.
3. GuilhermeBn198 commented on Aug 22, 2026

   

   GuilhermeBn198

   on Aug 22, 2026

   CollaboratorAuthor

   More actions

   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.
4. GuilhermeBn198

   closed this as completedon Aug 22, 2026
5. GuilhermeBn198

   added a commit that references this issue on Aug 23, 2026

   feat(slicing): slice the program with respect to the target before an…

   ...

   060f452