tacasv2a: --slice that keeps the suite valid (reach + assert)

[GuilhermeBn198]

Summary

tacasv2a, the first slice of the TACAS slicing work, making slicing per property. This PR fixes --slice for reachability and adds --slice for assert mode. It builds on #69 (tacasv1, AFL++; formerly #66). The base is develop, so the CI runs. Until #69 is merged, this diff also shows its commits; merge #69 first and they drop out. (It replaces #67, which GitHub closed when the head branch was renamed from tacas/slicing to feat/tacas-slicing.)

• Spec: docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md
• Plan: docs/superpowers/plans/2026-09-26-tacasv2a-slicing-reach-assert.md

The baseline for slicing is now tacasv1, not v15, and both sides use the same engine: AFL++ is the decided evolution, so nothing is calibrated against LibFuzzer.

What was wrong (diagnosed, not assumed)

In v15 the slice arm covered 412 tasks against 470 for the control. 57 of the 58 losses were in ECA. I sampled 12 of the lost tasks and ran them on the tacasv1 build. Two independent defects came out.

1. KLEE aborts on every slice that has a cut path.
   • sbt-slicer's --cutoff-diverging is on by default. It rewrites every path that cannot reach the criterion into a diverge: block that calls exit(0).
   • The help text says "abort()", but the dg source calls exit(0).
   • That call carries no debug location, while the program is compiled with -g.
   • Once KLEE links uClibc, exit has a body, and the LLVM verifier rejects the module: inlinable function call in a function with debug info must have a !dbg location → Broken module found.
   • KLEE never ran on those tasks. In v15 the exit(0) also ended the LibFuzzer session.
2. The suite found on the slice did not hold on the original program.
   • The slicer drops nondet reads that do not affect the target. ntdrivers/floppy.i.cil-1.c has 29 reads in the program and 10 in the slice.
   • TestCov runs the suite on the original program, where the vector shifts. The verdict is FAILED, but the suite is NOT_COVERED.

What changed

• The slicer runs with -cutoff-diverging=false.
• Every __VERIFIER_nondet_* function is a primary slicing criterion, so the read order is kept. The names come from a fixed list plus the program's own IR (opt -S), because no fixed list knows every name a benchmark declares (int128, …).
• --slice now also works with --check-asserts. The criteria are __VERIFIER_assert,__assert_fail, the two functions AssertPass instruments, and the weak stub has the (int cond) signature.
• The slice is logged in functions/blocks/instructions, from --statistics, not only in bytes.
• The pure pieces live in a new header-only modules/frontend/utils/slicer.hpp, which has unit tests.

Compared with Symbiotic (spec §4, read from its source):

• Symbiotic keeps the cutoff and never slices for Test-Comp properties in its main pipeline.
• What is new here: slicing that preserves the order in which inputs are consumed, so that a suite generated on the slice stays valid on the original program.

Results

12-task sample: the tasks v15's slice arm lost. Build tacas/slicing, 300 s budget, TestCov 300 s, one run per arm.

arm	covered
control (no slice)	12/12
slice, before this PR	6/12
slice, this PR	12/12; floppy is FAILED + COVERED

With this PR, the slice run finished faster than the control on 5 of the 9 ECA tasks. For example, Problem17_label55 gave FAILED in 51 s with the slice and UNKNOWN in 137 s without it. This is a diagnostic check, not an evaluation. The full Cover-Error comparison (1087 tasks, control vs slice, same build) is the tacasv2a run planned after merge (spec §7).

Test plan

• ctest: 10/10 (the new SlicerTest has 11 tests)
• tests/integration/test_testcomp_regressions.sh: 23/23. New sections:
  • 13: KLEE runs on a slice with a cut path. It failed before the fix with Broken module.
  • 14: the sliced suite keeps the original read order, giving [-2 42]. Before the fix it gave [42].
  • 15: assert mode slices towards the assertions and still finds the violation.
  • 16: nondet names that only the program declares are criteria too.
• CI TestCov step reproduced locally in the dev image: 16/16, 5/5, 6/6
• 12-task Cover-Error sample: slice 12/12
• Whole-branch review by a fresh reviewer: 0 Critical, 1 Important (fixed in ffad3e5d0: nondet names taken from the program), 5 Minor (deferred, listed below)
• CI

Deferred (minor, from the review)

• sbt-slicer prints "Statistics after" before its final cleanup, so the logged after-counts understate the reduction.
• The read-order guarantee holds for terminating executions. Standard control dependence can slice away a non-terminating loop that feeds nothing, and the comment and CHANGELOG wording should say so.
• There is no integration test yet for an SV-COMP-defined __VERIFIER_assert with --check-asserts --slice. It is safe according to the dg source.
• Test §14 reads only testcase-1.xml.
• A user target with parameters still gets a (void) weak stub. This predates the PR.

Decisions taken during execution

• The plan's test-13 program never produced a diverge: block: the slicer turns a plain return from main into safe_return. I replaced it with a small bounded ECA-shaped loop, which reproduces Broken module on the old code and gives FAILED on the new code.
• -cda ntscd and a "fixed" cutoff (keeping the cut but adding !dbg) were not adopted. The spec leaves both to measurement.

🤖 Generated with Claude Code