Skip to content

chore(benchexec): one tool version in the tool-info module #90

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
GuilhermeBn198 wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

chore(benchexec): one tool version in the tool-info module #90

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion docs/TESTCOMP-CHECKLIST.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ evidência que sustenta o estado declarado.
| **H1.1** Emissor de test suite XML | ✅ | `modules/frontend/test_suite/`. `--generate-test-suite` emite `metadata.xml` + `testcase-N.xml` no formato de intercâmbio. 13 testes unitários + 12 asserções de integração. **Custo real muito abaixo das 2 pw estimadas**: o runtime já registrava os valores em ordem de consumo, faltava só serializar |
| **H1.2** Conversor ktest→XML | ✅ | **Colapsou dentro do H1.1.** O log é escrito pelo binário instrumentado em tempo de execução, então já carrega os valores concretos do KLEE. Não precisou de conversor separado |
| **H1.3** Vetores de entrada por caminho | ✅ | **Resolvido por outro caminho que o planejado.** O KLEE já grava um `.ktest` por caminho explorado, com os objetos simbólicos em ordem de consumo; `ktest_reader.cpp` os lê. A alternativa (o runtime gravar um log por estado) foi **medida e descartada**: levou um run de 1s/`FALSE` para 100s/`SUCCEEDED` errado, porque cada escrita é chamada externa que o KLEE executa concretamente. 16 testes unitários fixam o parse contra bytes montados à mão |
| **H1.4** Empacotamento BenchExec / fm-tools | ✅ | `utils/moduleBenchExec/map2check_testcomp.py` (`BaseTool2`) + `utils/map2check-testcomp-wrapper.py`, ambos no zip de release. 15 asserções contra o benchexec real em `tests/integration/test_benchexec_toolinfo.py`. **Falta:** registrar em `fm-tools` (fora deste repositório). O `map2check.py` SV-COMP segue em `BaseTool` 1.x — obsoleto mas ainda presente no benchexec 3.35, então não está morto |
| **H1.4** Empacotamento BenchExec / fm-tools | ✅ | Um módulo tool-info só, o `map2check.py` do BenchExec (cópia em `utils/moduleBenchExec/map2check.py`), estendido em sosy-lab/benchexec#1352; um wrapper só, `utils/map2check-wrapper.py`, que escolhe verificação ou geração de testes pelo arquivo de propriedade. 24 asserções contra o benchexec real em `tests/integration/test_benchexec_toolinfo.py`. Registro em fm-tools: !1245, arquivo em DOI 10.5281/zenodo.23672409 |
| **H1.5** E2E no CI com TestCov | ✅ | Job `Test-Comp Validation (TestCov)`, 6/6 contra manifesto medido. Ver `tests/testcomp/` |

## H2 — Eficácia
Expand Down
4 changes: 2 additions & 2 deletions tests/integration/test_benchexec_toolinfo.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -172,8 +172,8 @@ def main():

silent_tool, silent_executable = fake_tool("")
silent_cmd = silent_tool.cmdline(silent_executable, [], task, limits)
check("a wrapper that does not tell its version gets no new options",
"--budget" not in silent_cmd, silent_cmd)
check("a wrapper that does not tell its version is taken as the current one",
"--budget" in silent_cmd, silent_cmd)

# --- determine_result ----------------------------------------------------
check("DONE as the last line is DONE",
Expand Down
17 changes: 6 additions & 11 deletions utils/moduleBenchExec/map2check.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@
#
# SPDX-License-Identifier: Apache-2.0

import functools
import os
import re

Expand Down Expand Up @@ -44,7 +43,11 @@ def executable(self, tool_locator):
self._version = 6
except ToolNotFoundException:
executable = tool_locator.find_executable("map2check-wrapper.py")
self._version = 7
# The Python wrapper (Map2Check 7 and later) reports the version,
# e.g., "v9.0.0-Songbirds:2026-10-13". If it does not, assume the
# current version.
match = re.match(r"v?(\d+)\.", self._version_from_tool(executable))
self._version = int(match.group(1)) if match else 9

return executable

Expand Down Expand Up @@ -87,7 +90,7 @@ def cmdline(self, executable, options, task, rlimits):
)
elif self._version > 6:
cmd = [executable] + options + ["-p", task.property_file]
if _major_version(executable) >= 9:
if self._version >= 9:
data_model = get_data_model_from_task(
task, {ILP32: "ILP32", LP64: "LP64"}
)
Expand Down Expand Up @@ -149,11 +152,3 @@ def determine_result(self, run):
status = "ERROR"

return status


@functools.lru_cache
def _major_version(executable):
"""The major version of Map2Check, or 0 if the wrapper does not tell."""
version = Tool._version_from_tool(executable)
match = re.match(r"v?(\d+)\.", version)
return int(match.group(1)) if match else 0
Loading