tacasv2b: --slice for memtrack/memcleanup, and two correctness fixes

[GuilhermeBn198]

Summary

tacasv2b makes --slice work for --memtrack and --memcleanup-property. It also fixes two correctness defects that the evaluation of this slicing exposed, and adds an SV-COMP MemSafety evaluation harness.

This PR builds on #68 (tacasv2a) → #69 (tacasv1), and the base is develop so the CI runs. Until #69 and #68 are merged, this diff also shows their commits. Merge order: #69, #68, then this PR.

• Spec: docs/superpowers/specs/2026-09-27-tacasv2b-slicing-memsafety-design.md
• Plan: docs/superpowers/plans/2026-09-27-tacasv2b-slicing-memsafety.md
• Every measurement round, with its comparison against the previous one: docs/reports/tacas-experiment-log.md (R6–R14)

What changed

• Slicing after instrumentation. In the memory modes, the slicer runs on the instrumented module (<hash>-output.bc), between callPass and linkLLVM. It does not run before instrumentation there, because the property lives in the runtime calls that MemoryTrackPass inserts. The criteria are:

  • every map2check_* call, so no check can be removed;
  • every __VERIFIER_nondet_* call;
  • every external function (declared, no body);
  • the memory intrinsics llvm.memcpy, llvm.memset and llvm.memmove.

  The entry point is __map2check_main__. The slicer invocation is shared with reach/assert through a private Caller::runSlicer.

• Refused when unsafe. If the instrumented module's runtime calls cannot be read, slicing is refused and the whole program is analysed. A slice without them as criteria would remove every check.

• Harness.

  • build_corpus.py gains --property memsafety|memcleanup. Categories are directory lists that mirror the SV-COMP sets, and each task carries its expected verdict and subproperty.
  • A new tests/memsafety/run_memsafety_evaluation.sh classifies each result as correct/wrong TRUE, correct/wrong FALSE (a FALSE counts only with the task's subproperty), unknown or error. The classifier has its own table test.
  • The CASTLE and Juliet runners accept EXTRA_FLAGS.

Correctness defects the evaluation exposed (fixed, with tests that failed first)

1. External calls were sliced away, giving a wrong TRUE.
   • A memory error can happen inside strcpy, memcpy or a lowered intrinsic. Nothing the runtime checks depends on that call, so the slicer removed it along with the bug.
   • Measured: CASTLE-787-2, and in R10 Juliet FN went from 117 to 169.
   • External functions and memory intrinsics are now criteria.
2. KLEE halting on its own --max-time reported TRUE. This bug predates this work (tacasv1, v15).
   • A halted run exits 0, exactly like a complete exploration. If one short path had written NONE, the verdict was TRUE: a reachable null dereference came back TRUE with no slicing at all.
   • Slicing exposed it on memsafety-cve frr.i and pacparser.i.
   • A halted KLEE now counts as a timeout: a recorded violation is kept, anything else is UNKNOWN.

Results: consolidated round R14 (both fixes, same build, control × slice)

corpus	control	slice
CASTLE (119)	TP 53, FN 14, FP 1	identical
SV-COMP MemSafety (50)	33 correct, wrong-true 2, wrong-false 3	33 correct, wrong-true 1, wrong-false 4
SV-COMP MemCleanup (10)	6 correct	identical; median time 14 s → 8 s
Juliet scope C (842)	TP 141, FN 117	TP 141, FN 117 (R10 without the fixes: 169)

• Reading: with the fixes, slicing introduces no new wrong TRUE. On these small programs it is neutral on correct answers.
• The individual changes:
  • Gains:
    • Juliet: 2 UNKNOWN → TP.
    • MemSafety: CWE122 …rand_18_bad went from TRUE (wrong) to FALSE-DEREF (correct).
  • Losses:
    • MemSafety csplit: correct → TIMEOUT.
    • Juliet CWE-121: 10 cases → ERROR/UNKNOWN. These were accidental detections: the out-of-bounds memcpy clobbered a neighbouring pointer, and the slice changes the stack layout.
  • busybox sleep-3 became FALSE-MEMTRACK. This is a pre-existing memtrack false positive, shown in R14 to occur without slicing too. It surfaces here only because the slice lets KLEE link.
• R14b re-runs the MemSafety slice arm with the final build, which adds intrinsics as criteria; see the log.

Test plan

• Integration tests/integration/test_testcomp_regressions.sh: 30 sections, all passing on an idle machine. Sections 10 and later cover this work:
  • detection kept for double free and leak;
  • no invented violation;
  • VLA fallback;
  • external call (strcpy);
  • halted KLEE;
  • memcpy intrinsic.
• ctest 10/10: SlicerTest 16, KtestReaderTest 21.
• tests/integration/test_memsafety_classifier.sh: 14/14.
• Evaluation rounds R8–R14 and R14b, recorded in docs/reports/tacas-experiment-log.md.
• Whole-branch review by a fresh reviewer. Its 3 Important findings are fixed (intrinsics, unsafe fallback, the Juliet classifier); the Minors are listed below.
• CI

Known limitations (deferred)

• MemoryTrackPass does not instrument LLVM 16 memory intrinsics. It matches the old typed names (llvm.memcpy.p0i8…), so memcpy/memset are never checked, with or without slicing. This predates this work and deserves its own fix; it changes the baseline.
• Other ways KLEE stops early (memory cap, solver timeouts) can still read as complete.
• The hybrid re-slices in every phase, which spends budget.
• Some integration tests only assert "not TRUE".
• Slicing is not sound with respect to non-termination. dg's standard control dependence is termination-insensitive.

🤖 Generated with Claude Code

[GuilhermeBn198]

R14b (memory slice arm re-run on the final build, with intrinsics as criteria): SV-COMP MemSafety 34 correct vs 33 in the control, wrong-TRUE 1 vs 2, no new error attributable to slicing (the remaining new wrong-false, busybox sleep-3, is a pre-existing memtrack false positive — see the log). MemCleanup identical, median time 14 s → 7 s. Details: docs/reports/tacas-experiment-log.md, section R14b.