feat(testcomp): BenchExec packaging, and always emit a test suite (H1.4)

[GuilhermeBn198]

Closes H1.4, the last unstarted item in H1 — conformance, which is the front that decides whether Map2Check can be submitted to Test-Comp at all.

1. The suite is now emitted for every outcome

Emission lived inside if (foundViolation). A run that decided nothing left no test-suite/ directory at all — and the competition harness reads an absent directory as a tool that crashed, not as an honest zero.

metadata.xml is now always written. foundViolation decides whether the suite carries a test case, not whether the suite exists.

run	result
violation found	metadata.xml + testcase-1.xml
nothing found	metadata.xml, 0 test cases

2. utils/map2check-testcomp-wrapper.py

Separate from the SV-COMP wrapper deliberately. That one answers "does this program satisfy the property" and prints a verdict; this one produces an artefact and lets TestCov score it. Different verdict vocabulary, different exit codes, different output — folding both into one script would mean behaviour depending on a property string in two unrelated ways.

It resolves the binary against its own path, not ./map2check: BaseTool2 dropped the working_directory() hook the old wrapper relied on, so the process now starts in the benchmark's directory, not the tool's. (The binary must still be named map2check — it derives MAP2CHECK_PATH from /proc/self/exe.)

3. utils/moduleBenchExec/map2check_testcomp.py

The tool-info module, in BaseTool2, written against the introspected benchexec 3.35 API rather than from memory — the whole risk here is the API not being what we assumed.

Two decisions worth calling out:

• cover-branches is refused, not accepted. Branch coverage needs one test case per input vector and the runtime writes one nondet log per run (H1.3). Accepting it would look like participation while scoring zero and hiding the reason. Raising UnsupportedFeatureException makes BenchExec skip the task instead.
• The harness walltime becomes the tool's own budget. So it is Map2Check that stops and finishes writing metadata.xml, rather than the harness killing it mid-write and leaving a truncated file — which is worse than an empty suite.

determine_result only distinguishes ran from broke. Claiming anything stronger would be the tool self-reporting whether its suite covers the error, which is exactly what the competition does not allow.

4. tests/integration/test_benchexec_toolinfo.py — 15 assertions

Nothing in this repository exercised the tool-info module, and its failure mode is nasty: it surfaces on competition infrastructure, days after submission, as every task erroring out. Tested against the real benchexec package, not a stub.

PASS the module is a BaseTool2, not the deprecated BaseTool
PASS the wrapper is the executable, not the raw binary
PASS the walltime limit becomes the tool's own budget
PASS a task declaring ILP32 is honoured
PASS cover-branches is refused rather than faked
PASS an SV-COMP CHECK property is refused by the Test-Comp module
PASS a timeout still counts as DONE, because the suite was written
... 15 passed, 0 failed

Wired into the TestCov job, which already has benchexec (testcov depends on it).

5. scripts/package-release.sh

The wrapper goes into the release zip, because the module's REQUIRED_PATHS declares it and BenchExec copies exactly those paths to the execution node — a file missing from the zip becomes an error on competition infrastructure, not here.

Verification

Against a full build and install, not the pieces in isolation:

E2E violation     -> metadata.xml + testcase-1.xml, <specification> copied verbatim
E2E no violation  -> metadata.xml, 0 test cases
tool-info         -> 15/15
TestCov corpus    -> 6/6

The TestCov corpus mattered most here: the two NOT_COVERED cases used to take the runner's "no test suite produced" shortcut, and now reach TestCov with an empty suite. TestCov handles that and reports Result: UNKNOWN, so the gate holds — this was the one way the change could have broken it.

Not in this PR

• Registering in fm-tools — lives outside this repository.
• Migrating map2check.py (SV-COMP) to BaseTool2 — it is on BaseTool 1.x, which is deprecated but still present in benchexec 3.35, so it is legacy rather than dead. Separate change, separate risk.
• H1.3 / H2.5 (cover-branches) — needs a per-input nondet log. Now the declared bottleneck in the checklist, and the reason the tool-info refuses that property.