diff --git a/CHANGELOG.md b/CHANGELOG.md index c1d035f7d..ff411b8a9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,12 @@ The format loosely follows [Keep a Changelog](https://keepachangelog.com/en/1.0. ### Changed - Replaced LibFuzzer with AFL++ 4.40c (persistent, PCGUARD) as the fuzzing engine. +- tacasv2a: `--slice` no longer crashes KLEE and its test suites stay valid + on the original program. The slicer runs with `-cutoff-diverging=false` + (the cutoff's `exit(0)` had no debug location and KLEE rejected the + module), and every `__VERIFIER_nondet_*` function is a slicing criterion, + so the read order is preserved. `--slice` now also works with + `--check-asserts`. The slice is logged in functions/blocks/instructions. - Migrated the toolchain from LLVM 6.0 to LLVM 16, moving all instrumentation passes (`modules/backend/pass/`) to the New Pass Manager and opaque pointers. - Migrated the codebase to C++17 (CMake `CMAKE_CXX_STANDARD` 11 → 17, required by LLVM 16 headers). - Upgraded KLEE to 3.1. diff --git a/docs/superpowers/plans/2026-09-26-tacasv2a-slicing-reach-assert.md b/docs/superpowers/plans/2026-09-26-tacasv2a-slicing-reach-assert.md new file mode 100644 index 000000000..d184904bc --- /dev/null +++ b/docs/superpowers/plans/2026-09-26-tacasv2a-slicing-reach-assert.md @@ -0,0 +1,752 @@ +# tacasv2a — Slicing for reach/assert that keeps the suite valid: Implementation Plan + +> **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (`- [ ]`) syntax for tracking. + +**Goal:** Make `--slice` stop crashing KLEE and stop producing test suites that are invalid on the original program. Also extend `--slice` to assert mode. + +**Architecture:** Slicing stays where it is: in `Caller::sliceWithRespectToTarget`, before instrumentation. The pure pieces are: +- the criteria list, built from the target plus every `__VERIFIER_nondet_*` function; +- the weak-stub source; +- the parser for the slicer's `--statistics` output. + +They move into a new header-only unit `modules/frontend/utils/slicer.hpp`, so they can be unit-tested without a build of the whole tool. The Caller then passes `-cutoff-diverging=false --statistics` and logs the counts. `map2check.cpp` enables the assert-mode criterion. + +**Tech Stack:** C++17, LLVM 16, sbt-slicer (dg) pinned in `Dockerfile.dev`, GTest, bash integration tests. Build and run everything inside the dev image (`map2check-dev:aflpp`, built from `Dockerfile.dev`); the host has no clang, cmake or ninja. + +**Spec:** `docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md` + +## Global Constraints + +- Branch `tacas/slicing` (created from `tacas/aflpp`); the baseline is tacasv1. Never target LibFuzzer. +- Cutoff: `-cutoff-diverging=false`. +- Reachability criterion: `` plus every known `__VERIFIER_nondet_*` function. +- Assert criterion: `__VERIFIER_assert,__assert_fail` plus the same nondet functions (AssertPass instruments both). +- Slice before instrumentation (unchanged). Keep the weak stub for the criterion function. +- Other slicer flags (`--pta`, `--cda`, `--undefined-funs`) stay at their defaults in this stage. +- Pass `--statistics` to the slicer, and log globals/functions/blocks/instructions before → after, plus bytes. +- C++: Google style (`.clang-format`), `` (never boost). Commit messages end with `Co-Authored-By: Claude Opus 5.5 (1M context) `. + +## Review Focus + +- **A program that declares no nondet function at all** (`no_input.c`-like). The criteria must still be the target alone plus names that do not exist, and the slicer accepts those silently (verified). Pinned in Task 1. +- **`--slice` in assert mode on a program that only declares `__VERIFIER_assert`.** The weak stub must have the `(int)` signature or `llvm-link` rejects the type. Pinned in Task 3. +- **A slicer build whose `--statistics` prints nothing, or a different format.** The log must fall back to bytes only and never print zeros as if measured. Pinned in Task 1 (parser returns `found=false`). +- **A program with a nondet read that is irrelevant to the target and consumed before the relevant one.** The suite must carry both values, in the original order. Pinned in Task 2. +- **A program whose non-target branch returns early** (the path the cutoff used to rewrite). KLEE must run and report FAILED, not abort on a broken module. Pinned in Task 2. + +--- + +## File Structure + +- Create `modules/frontend/utils/slicer.hpp`, header-only and pure (no I/O). It holds `nondetFunctionNames()`, `slicingCriteria()`, `targetStubSource()`, `SlicerStatistics`, `parseSlicerStatistics()` and `describeSlice()`. +- Create `tests/unit/frontend/SlicerTest.cpp` with the GTest unit tests for `slicer.hpp`. +- Modify `tests/unit/frontend/CMakeLists.txt` to register `SlicerTest`. +- Modify `modules/frontend/caller.cpp` so that `sliceWithRespectToTarget` uses `slicer.hpp` and passes the new flags. +- Modify `modules/frontend/caller.hpp` to update the doc comment of `sliceWithRespectToTarget`; the signature stays the same. +- Modify `modules/frontend/map2check.cpp` for the `--slice` gating (reach + assert) and the help text. +- Modify `tests/integration/test_testcomp_regressions.sh`: new slicing sections, and the refusal-message check updated. +- Modify `CHANGELOG.md` to add a tacasv2a entry. + +--- + +### Task 1: Pure slicing helpers (`slicer.hpp`) with unit tests + +**Files:** +- Create: `modules/frontend/utils/slicer.hpp` +- Create: `tests/unit/frontend/SlicerTest.cpp` +- Modify: `tests/unit/frontend/CMakeLists.txt` (append) + +**Interfaces:** +- Produces (namespace `Map2Check`): + - `const std::vector& nondetFunctionNames();` + - `std::string slicingCriteria(const std::vector& primary);` returns the comma-joined `primary` followed by every nondet name. + - `std::string targetStubSource(const std::string& function);` returns a one-line C weak definition with the right signature. + - `struct SlicerCounts { unsigned globals = 0, functions = 0, blocks = 0, instructions = 0; };` + - `struct SlicerStatistics { bool found = false; SlicerCounts before, after; };` + - `SlicerStatistics parseSlicerStatistics(const std::string& slicerOutput);` + - `std::string describeSlice(const std::string& criterion, const SlicerStatistics& stats, uintmax_t bytesBefore, uintmax_t bytesAfter);` + +- [ ] **Step 1: Write the failing unit tests** + +Create `tests/unit/frontend/SlicerTest.cpp`: + +```cpp +/** + * Copyright (C) 2014 - 2026 Map2Check tool + * This file is part of the Map2Check tool, and is made available under + * the terms of the GNU General Public License version 2. + * + * SPDX-License-Identifier: (GPL-2.0) + **/ + +#include + +#include +#include +#include + +#include "../../../modules/frontend/utils/slicer.hpp" + +// The suite is generated on the slice and run by TestCov on the ORIGINAL +// program, so every nondet read the original performs must survive slicing. +TEST(SlicingCriteria, AppendsEveryNondetFunctionAfterThePrimary) { + const std::string criteria = Map2Check::slicingCriteria({"reach_error"}); + EXPECT_EQ(criteria.rfind("reach_error,", 0), 0u); + for (const std::string& name : Map2Check::nondetFunctionNames()) { + EXPECT_NE(criteria.find("," + name), std::string::npos) << name; + } +} + +TEST(SlicingCriteria, KeepsSeveralPrimariesInOrder) { + const std::string criteria = + Map2Check::slicingCriteria({"__VERIFIER_assert", "__assert_fail"}); + EXPECT_EQ(criteria.rfind("__VERIFIER_assert,__assert_fail,", 0), 0u); +} + +TEST(NondetFunctionNames, CoversWhatNonDetPassInstruments) { + const auto& names = Map2Check::nondetFunctionNames(); + for (const char* type : {"bool", "char", "uchar", "short", "ushort", "int", + "uint", "unsigned", "long", "ulong", "size_t", + "loff_t", "sector_t", "pointer", "pchar", "double"}) { + const std::string name = std::string("__VERIFIER_nondet_") + type; + EXPECT_NE(std::find(names.begin(), names.end(), name), names.end()) << name; + } +} + +TEST(TargetStubSource, VoidTargetGetsAVoidStub) { + EXPECT_EQ(Map2Check::targetStubSource("reach_error"), + "void __attribute__((weak)) reach_error(void) {}\n"); +} + +// __VERIFIER_assert takes the condition; a (void) stub would not link against +// the program's own declaration. +TEST(TargetStubSource, AssertStubTakesTheCondition) { + EXPECT_EQ(Map2Check::targetStubSource("__VERIFIER_assert"), + "void __attribute__((weak)) __VERIFIER_assert(int cond) {}\n"); +} + +TEST(ParseSlicerStatistics, ReadsBeforeAndAfter) { + const std::string output = + "Statistics before Globals/Functions/Blocks/Instr.: 37 97 2215 10764\n" + "[llvm-slicer] Sliced away 1454 from 4227 nodes in DG\n" + "Statistics after Globals/Functions/Blocks/Instr.: 37 38 444 2989\n"; + const Map2Check::SlicerStatistics stats = + Map2Check::parseSlicerStatistics(output); + ASSERT_TRUE(stats.found); + EXPECT_EQ(stats.before.functions, 97u); + EXPECT_EQ(stats.before.blocks, 2215u); + EXPECT_EQ(stats.before.instructions, 10764u); + EXPECT_EQ(stats.after.globals, 37u); + EXPECT_EQ(stats.after.functions, 38u); + EXPECT_EQ(stats.after.instructions, 2989u); +} + +// A slicer that prints no statistics must not be reported as having sliced +// everything away. +TEST(ParseSlicerStatistics, MissingLinesAreNotFound) { + EXPECT_FALSE(Map2Check::parseSlicerStatistics("").found); + EXPECT_FALSE(Map2Check::parseSlicerStatistics( + "Statistics before Globals/Functions/Blocks/Instr.: 1 2 3 4\n") + .found); +} + +TEST(DescribeSlice, ReportsCountsWhenFound) { + Map2Check::SlicerStatistics stats; + stats.found = true; + stats.before = {37, 97, 2215, 10764}; + stats.after = {37, 38, 444, 2989}; + EXPECT_EQ(Map2Check::describeSlice("reach_error", stats, 184164, 171708), + "Sliced with respect to reach_error: 97/2215/10764 -> 38/444/2989 " + "functions/blocks/instructions (184164 -> 171708 bytes of " + "bitcode)"); +} + +TEST(DescribeSlice, FallsBackToBytesWithoutStatistics) { + EXPECT_EQ(Map2Check::describeSlice("reach_error", {}, 10, 8), + "Sliced with respect to reach_error: 10 -> 8 bytes of bitcode"); +} +``` + +Append to `tests/unit/frontend/CMakeLists.txt`: + +```cmake + +add_executable(SlicerTest + SlicerTest.cpp +) +map2check_test(SlicerTest) +``` + +- [ ] **Step 2: Run the tests and confirm they fail to compile** + +Run inside the dev image: +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c \ + 'mkdir -p /workspace/build_ut && cd /workspace/build_ut && cmake .. -G Ninja -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm -DENABLE_TEST=ON >/dev/null && ninja SlicerTest 2>&1 | tail -5' +``` +Expected: FAIL with `fatal error: '../../../modules/frontend/utils/slicer.hpp' file not found`. + +- [ ] **Step 3: Implement `slicer.hpp`** + +Create `modules/frontend/utils/slicer.hpp`: + +```cpp +/** + * Copyright (C) 2014 - 2026 Map2Check tool + * This file is part of the Map2Check tool, and is made available under + * the terms of the GNU General Public License version 2. + * + * SPDX-License-Identifier: (GPL-2.0) + **/ + +#ifndef MODULES_FRONTEND_UTILS_SLICER_HPP_ +#define MODULES_FRONTEND_UTILS_SLICER_HPP_ + +#include +#include +#include +#include +#include + +namespace Map2Check { + +/** Every __VERIFIER_nondet_* function the slice must keep. + * + * The suite is generated on the slice, but TestCov runs it on the ORIGINAL + * program. A nondet call the slicer drops -- its value does not reach the + * criterion -- is still consumed by the original, so the vector shifts and + * the suite stops covering (measured: ntdrivers/floppy.i.cil-1.c, 29 reads in + * the program and 10 in the slice; FAILED, NOT_COVERED). Keeping these calls + * as criteria keeps the consumption order. + * + * The first sixteen are what NonDetPass instruments; the rest are SV-COMP + * names it does not model yet, kept so their order is not lost either. The + * slicer accepts names the program does not use. */ +inline const std::vector& nondetFunctionNames() { + static const std::vector names = { + "__VERIFIER_nondet_bool", "__VERIFIER_nondet_char", + "__VERIFIER_nondet_uchar", "__VERIFIER_nondet_short", + "__VERIFIER_nondet_ushort", "__VERIFIER_nondet_int", + "__VERIFIER_nondet_uint", "__VERIFIER_nondet_unsigned", + "__VERIFIER_nondet_long", "__VERIFIER_nondet_ulong", + "__VERIFIER_nondet_size_t", "__VERIFIER_nondet_loff_t", + "__VERIFIER_nondet_sector_t", "__VERIFIER_nondet_pointer", + "__VERIFIER_nondet_pchar", "__VERIFIER_nondet_double", + "__VERIFIER_nondet_float", "__VERIFIER_nondet_longlong", + "__VERIFIER_nondet_ulonglong", "__VERIFIER_nondet__Bool", + "__VERIFIER_nondet_u8", "__VERIFIER_nondet_u16", + "__VERIFIER_nondet_u32", "__VERIFIER_nondet_charp"}; + return names; +} + +/** The -c argument: the primary criteria, then every nondet function. */ +inline std::string slicingCriteria(const std::vector& primary) { + std::ostringstream criteria; + bool first = true; + for (const std::string& name : primary) { + criteria << (first ? "" : ",") << name; + first = false; + } + for (const std::string& name : nondetFunctionNames()) { + criteria << (first ? "" : ",") << name; + first = false; + } + return criteria.str(); +} + +/** A weak definition of the criterion function, restoring the body the + * slicer removes without displacing a real one. The signature must match + * the program's declaration, or llvm-link rejects the module. */ +inline std::string targetStubSource(const std::string& function) { + if (function == "__VERIFIER_assert") { + return "void __attribute__((weak)) __VERIFIER_assert(int cond) {}\n"; + } + return "void __attribute__((weak)) " + function + "(void) {}\n"; +} + +struct SlicerCounts { + unsigned globals = 0; + unsigned functions = 0; + unsigned blocks = 0; + unsigned instructions = 0; +}; + +struct SlicerStatistics { + bool found = false; // both the "before" and the "after" line were read + SlicerCounts before; + SlicerCounts after; +}; + +/** Reads sbt-slicer's --statistics lines: + * Statistics before Globals/Functions/Blocks/Instr.: 37 97 2215 10764 + * Statistics after Globals/Functions/Blocks/Instr.: 37 38 444 2989 */ +inline SlicerStatistics parseSlicerStatistics(const std::string& slicerOutput) { + static const std::regex line( + R"(Statistics (before|after) Globals/Functions/Blocks/Instr\.:\s+)" + R"((\d+)\s+(\d+)\s+(\d+)\s+(\d+))"); + SlicerStatistics stats; + bool sawBefore = false; + bool sawAfter = false; + for (std::sregex_iterator it(slicerOutput.begin(), slicerOutput.end(), line), + end; + it != end; ++it) { + const std::smatch& m = *it; + SlicerCounts counts; + counts.globals = static_cast(std::stoul(m[2])); + counts.functions = static_cast(std::stoul(m[3])); + counts.blocks = static_cast(std::stoul(m[4])); + counts.instructions = static_cast(std::stoul(m[5])); + if (m[1] == "before") { + stats.before = counts; + sawBefore = true; + } else { + stats.after = counts; + sawAfter = true; + } + } + stats.found = sawBefore && sawAfter; + return stats; +} + +/** The one log line a slice produces. Counts when the slicer reported them, + * bytes always -- a slice narrows the question being answered, and this line + * is the only visible sign of how much was dropped. */ +inline std::string describeSlice(const std::string& criterion, + const SlicerStatistics& stats, + uintmax_t bytesBefore, uintmax_t bytesAfter) { + std::ostringstream text; + text << "Sliced with respect to " << criterion << ": "; + if (stats.found) { + text << stats.before.functions << "/" << stats.before.blocks << "/" + << stats.before.instructions << " -> " << stats.after.functions << "/" + << stats.after.blocks << "/" << stats.after.instructions + << " functions/blocks/instructions (" << bytesBefore << " -> " + << bytesAfter << " bytes of bitcode)"; + } else { + text << bytesBefore << " -> " << bytesAfter << " bytes of bitcode"; + } + return text.str(); +} + +} // namespace Map2Check + +#endif // MODULES_FRONTEND_UTILS_SLICER_HPP_ +``` + +- [ ] **Step 4: Run the tests and confirm they pass** + +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c \ + 'cd /workspace/build_ut && ninja SlicerTest >/dev/null && ./tests/unit/frontend/SlicerTest 2>&1 | tail -3' +``` +Expected: `[ PASSED ] 9 tests.` (If the binary is elsewhere, find it with `find /workspace/build_ut -name SlicerTest -type f`.) + +- [ ] **Step 5: Commit** + +```bash +git add modules/frontend/utils/slicer.hpp tests/unit/frontend/SlicerTest.cpp tests/unit/frontend/CMakeLists.txt +git commit -m "feat(tacasv2a): pure slicing helpers -- criteria, stub, statistics + +Co-Authored-By: Claude Opus 5.5 (1M context) " +``` + +--- + +### Task 2: Slice without cutoff, keep the nondets, log the statistics + +**Files:** +- Modify: `modules/frontend/caller.cpp`, in `Caller::sliceWithRespectToTarget` (starts around line 179: the command construction around lines 218-222, the success log around lines 243-245, and the stub around lines 262-268) +- Modify: `modules/frontend/caller.hpp:133-136` (doc comment only) +- Test: `tests/integration/test_testcomp_regressions.sh`, new section 13 inserted **before** the final `echo " ---"` summary lines + +**Interfaces:** +- Consumes: `Map2Check::slicingCriteria`, `Map2Check::targetStubSource`, `Map2Check::parseSlicerStatistics`, `Map2Check::describeSlice` from Task 1. +- Produces: the log line `Sliced with respect to : …` (the integration tests grep the `Sliced with respect to` prefix). `sliceWithRespectToTarget` gains a second parameter, `const std::vector& criteria`, the primary criteria; the first stays `targetFunction`, used for the stub and the log. Task 3 calls it with `{"__VERIFIER_assert", "__assert_fail"}`. + +- [ ] **Step 1: Write the failing integration tests** + +In `tests/integration/test_testcomp_regressions.sh`, insert this block immediately before the lines `echo " ---"` / `echo " Results: ..."` at the end: + +```bash +# --- 13. a slice must leave KLEE something it can run ------------------------- +# sbt-slicer's --cutoff-diverging (default on) rewrites every path that cannot +# reach the criterion into a `diverge:` block calling exit(0) -- with no debug +# location. The program is compiled with -g; once KLEE links uClibc, exit has a +# body, and the verifier rejects the module ("inlinable function call in a +# function with debug info must have a !dbg location"). KLEE aborted before +# executing anything, on every sliced task with a cut path: the slice arm of +# the v15 campaign ran without its symbolic engine. +mkdir -p "$WORK/cut" +cat > "$WORK/cut/cut.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void reach_error(void); +int main(void) { + int x = __VERIFIER_nondet_int(); + if (x == 3) { return 1; } + if (x == 7) { reach_error(); } + return 0; +} +EOF +( cd "$WORK/cut" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --slice \ + --nondet-generator symex --timeout 45 cut.c ) > "$WORK/cut/run.log" 2>&1 +if grep -q "Broken module" "$WORK/cut/run.log"; then + fail "slice + KLEE" "KLEE rejected the sliced module (cutoff exit without !dbg)" +elif grep -q "VERIFICATION FAILED" "$WORK/cut/run.log"; then + ok "KLEE runs on the slice and reaches the target" +else + fail "slice + KLEE" "no FAILED verdict on a trivially reachable target" + grep -E "Sliced|Exited klee|VERIFICATION" "$WORK/cut/run.log" | sed 's/^/ /' +fi + +# --- 14. a suite found on the slice must hold on the original ---------------- +# TestCov runs the suite on the ORIGINAL program. A nondet read the slicer +# dropped -- its value does not reach the target -- is still consumed there, +# so the vector shifts: measured on ntdrivers/floppy.i.cil-1.c, FAILED and +# NOT_COVERED. The slice keeps every nondet call, so both values appear, in +# the original order. +mkdir -p "$WORK/order" +cp "$WORK/one/reach.prp" "$WORK/order/" +cat > "$WORK/order/order.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void reach_error(void); +int main(void) { + int a = __VERIFIER_nondet_int(); + int b = __VERIFIER_nondet_int(); + if (b == 42) { reach_error(); } + return a; +} +EOF +( cd "$WORK/order" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --slice \ + --nondet-generator symex --generate-test-suite --property-file reach.prp \ + --timeout 60 order.c ) > "$WORK/order/run.log" 2>&1 +order_inputs=$(sed -n 's:.*\(.*\).*:\1:p' \ + "$WORK/order/test-suite/testcase-1.xml" 2>/dev/null | tr '\n' ' ') +if [ "$(echo $order_inputs | wc -w)" -eq 2 ] && \ + [ "$(echo $order_inputs | awk '{print $2}')" = "42" ]; then + ok "the sliced suite keeps the original read order [$order_inputs]" +else + fail "slice read order" "expected 2 inputs ending in 42, got [$order_inputs]" +fi +``` + +- [ ] **Step 2: Build the current code and confirm the new tests fail** + +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c ' + mkdir -p /workspace/build_aflpp && cd /workspace/build_aflpp && + cmake .. -G Ninja -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm -DCMAKE_INSTALL_PREFIX=/workspace/build_aflpp/install >/dev/null && + ninja >/dev/null && ninja install >/dev/null && + mkdir -p install/lib/klee && ln -sfn /opt/klee/lib/klee/runtime install/lib/klee/runtime && + ln -sfn /usr/lib/llvm-16/lib/clang install/lib/clang && + cd /workspace && MAP2CHECK_PATH=/workspace/build_aflpp/install bash tests/integration/test_testcomp_regressions.sh 2>&1 | grep -E "FAIL|PASS KLEE runs|read order|Results"' +``` +Expected: both `FAIL slice + KLEE: KLEE rejected the sliced module …` and `FAIL slice read order: …`. + +- [ ] **Step 3: Implement the Caller change** + +In `modules/frontend/caller.cpp`, add `#include "utils/slicer.hpp"` next to the other `utils/` includes. + +Change the signature (definition and declaration) to: + +```cpp +bool Caller::sliceWithRespectToTarget(const std::string &targetFunction, + const std::vector &criteria) +``` + +and in `caller.hpp` replace the declaration and its comment with: + +```cpp + /** Runs sbt-slicer over the compiled (not yet instrumented) bitcode. + * + * `criteria` are the primary slicing criteria (the target function, or the + * assert functions); every __VERIFIER_nondet_* function is added to them so + * the suite found on the slice stays valid on the original program. The + * cutoff of diverging paths is off: its exit(0) carries no debug location + * and KLEE rejects the module. `targetFunction` gets its body back through a + * weak stub. Returns false if the slicer is unavailable or produced nothing + * usable, leaving the original bitcode in place. */ + bool sliceWithRespectToTarget(const std::string& targetFunction, + const std::vector& criteria); +``` + +Replace the command construction: + +```cpp + command << "timeout -k " << Map2Check::killGracePeriod << " " << static_cast(sliceBudget) + << " " << slicer << " -c " << targetFunction + << " --entry=main -o " << output << " " + << input << " > slicer.output 2>&1"; +``` + +with: + +```cpp + // -cutoff-diverging=false: the cutoff rewrites every path that cannot reach + // the criterion into exit(0) with no debug location, and once KLEE links + // uClibc the verifier rejects the module ("Broken module found") -- KLEE + // never ran on a sliced task with a cut path (tacasv2a spec, defect 1). + // + // The nondet functions ride along as criteria so that every read the + // original program performs survives; the suite is generated on the slice + // and replayed on the original (defect 2). + // + // --statistics: counts before and after, logged below. + command << "timeout -k " << Map2Check::killGracePeriod << " " + << static_cast(sliceBudget) << " " << slicer << " -c " + << Map2Check::slicingCriteria(criteria) + << " --entry=main -cutoff-diverging=false --statistics -o " << output + << " " << input << " > slicer.output 2>&1"; +``` + +Replace the success log: + +```cpp + Map2Check::Log::Info("Sliced with respect to " + targetFunction + ": " + + std::to_string(before) + " -> " + + std::to_string(after) + " bytes of bitcode"); +``` + +with: + +```cpp + std::ifstream slicerLog("slicer.output"); + std::stringstream slicerText; + slicerText << slicerLog.rdbuf(); + std::string criterionLabel; + for (const std::string &name : criteria) { + criterionLabel += (criterionLabel.empty() ? "" : ",") + name; + } + Map2Check::Log::Info(Map2Check::describeSlice( + criterionLabel, Map2Check::parseSlicerStatistics(slicerText.str()), + before, after)); +``` + +Replace the stub text: + +```cpp + stub << "void __attribute__((weak)) " << targetFunction << "(void) {}\n"; +``` + +with: + +```cpp + stub << Map2Check::targetStubSource(targetFunction); +``` + +In `modules/frontend/map2check.cpp`, change the one existing call so it still compiles and keeps today's behaviour for reachability: + +```cpp + caller->sliceWithRespectToTarget(args.function, {args.function}); +``` + +Make sure `caller.cpp` includes `` and `` (it already uses `std::ostringstream` and `std::ifstream`; add whichever is missing). + +- [ ] **Step 4: Rebuild and run the integration tests plus the unit tests** + +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c ' + cd /workspace/build_aflpp && ninja >/dev/null && ninja install >/dev/null && + cd /workspace && MAP2CHECK_PATH=/workspace/build_aflpp/install bash tests/integration/test_testcomp_regressions.sh 2>&1 | grep -E "FAIL|KLEE runs|read order|sliced with respect|Results"' +``` +Expected: `PASS KLEE runs on the slice and reaches the target`, `PASS the sliced suite keeps the original read order [ 42 ]`, `PASS the program was sliced with respect to the target`, and `Results: 21 passed, 0 failed`. + +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c 'cd /workspace/build_ut && ninja >/dev/null && ctest 2>&1 | tail -3' +``` +Expected: `100% tests passed`. + +- [ ] **Step 5: Commit** + +```bash +git add modules/frontend/caller.cpp modules/frontend/caller.hpp modules/frontend/map2check.cpp tests/integration/test_testcomp_regressions.sh +git commit -m "fix(tacasv2a): slice without cutoff and keep every nondet read + +The cutoff's exit(0) carries no !dbg and KLEE rejected every sliced +module with a cut path; nondet reads the slicer dropped shifted the +suite on the original program. Both are integration-tested now, and the +slice is logged in functions/blocks/instructions, not only bytes. + +Co-Authored-By: Claude Opus 5.5 (1M context) " +``` + +--- + +### Task 3: `--slice` in assert mode + +**Files:** +- Modify: `modules/frontend/map2check.cpp`, the `if (args.sliceProgram)` block (around lines 519-528) and the `("slice", …)` help text (around lines 748-750) +- Test: `tests/integration/test_testcomp_regressions.sh`, section 12's refusal check, plus a new section 15 before the summary +- Modify: `CHANGELOG.md` (top entry) + +**Interfaces:** +- Consumes: `Caller::sliceWithRespectToTarget(const std::string&, const std::vector&)` from Task 2. +- Produces: in assert mode the log line is `Sliced with respect to __VERIFIER_assert,__assert_fail: …`, and the refusal message becomes `--slice applies to reachability and assert only`. + +- [ ] **Step 1: Write the failing tests** + +In section 12 of `tests/integration/test_testcomp_regressions.sh`, change the refusal check's grep from `"applies to reachability only"` to `"applies to reachability and assert only"`. + +Insert before the summary lines (after section 14): + +```bash +# --- 15. assert mode slices towards the assertions ---------------------------- +# AssertPass instruments __VERIFIER_assert and __assert_fail, so those are the +# criteria. The program only DECLARES __VERIFIER_assert: the weak stub must +# take the condition, or llvm-link rejects the (void) definition. +mkdir -p "$WORK/assert" +cat > "$WORK/assert/assert.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void __VERIFIER_assert(int cond); +int main(void) { + int a = __VERIFIER_nondet_int(); + int b = __VERIFIER_nondet_int(); + if (a > 0) { a = a - 1; } + __VERIFIER_assert(b != 77); + return a; +} +EOF +( cd "$WORK/assert" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --check-asserts --slice --nondet-generator symex --timeout 45 assert.c ) \ + > "$WORK/assert/run.log" 2>&1 +if grep -q "Sliced with respect to __VERIFIER_assert,__assert_fail" "$WORK/assert/run.log" && \ + grep -q "VERIFICATION FAILED" "$WORK/assert/run.log"; then + ok "assert mode slices towards the assertions and still finds the violation" +else + fail "assert slice" "no assert-criterion slice, or the violation was lost" + grep -E "Sliced|slice|VERIFICATION" "$WORK/assert/run.log" | sed 's/^/ /' +fi +``` + +- [ ] **Step 2: Run them and confirm they fail** + +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c ' + cd /workspace && MAP2CHECK_PATH=/workspace/build_aflpp/install bash tests/integration/test_testcomp_regressions.sh 2>&1 | grep -E "FAIL|Results"' +``` +Expected: `FAIL slice mode guard: …` (old message) and `FAIL assert slice: …`. + +- [ ] **Step 3: Implement the gating** + +Replace the block: + +```cpp + if (args.sliceProgram) { + if (args.mode == Map2Check::Map2CheckMode::REACHABILITY_MODE) { + caller->sliceWithRespectToTarget(args.function, {args.function}); + } else { + Map2Check::Log::Warning( + "--slice applies to reachability only: there is no criterion to " + "slice towards when the goal is coverage or a memory property. " + "Analysing the whole program."); + } + } +``` + +with: + +```cpp + // Reachability slices towards the target; assert towards the two functions + // AssertPass instruments. Memory properties and overflow need their own + // criteria (tacasv2b/2c); coverage has none -- every branch is the goal. + if (args.sliceProgram) { + if (args.mode == Map2Check::Map2CheckMode::REACHABILITY_MODE) { + caller->sliceWithRespectToTarget(args.function, {args.function}); + } else if (args.mode == Map2Check::Map2CheckMode::ASSERT_MODE) { + caller->sliceWithRespectToTarget("__VERIFIER_assert", + {"__VERIFIER_assert", "__assert_fail"}); + } else { + Map2Check::Log::Warning( + "--slice applies to reachability and assert only: there is no " + "criterion to slice towards when the goal is coverage or a memory " + "or overflow property. Analysing the whole program."); + } + } +``` + +Replace the help text: + +```cpp + ("slice", + "\tslice the program with respect to the target before analysing it " + "(reachability only; needs sbt-slicer)") +``` + +with: + +```cpp + ("slice", + "\tslice the program with respect to the target (reachability) or " + "the assertions (--check-asserts) before analysing it; needs " + "sbt-slicer") +``` + +Update the comment block right above `if (args.sliceProgram)` that ends with "Reachability only. Slicing needs a criterion, and Cover-Branches has none -- every branch is the goal. Asking elsewhere is refused, not ignored." so that its last paragraph reads: "Reachability and assert. Slicing needs a criterion, and Cover-Branches has none -- every branch is the goal. Asking elsewhere is refused, not ignored." + +- [ ] **Step 4: Rebuild and run everything** + +```bash +docker run --rm -v $(pwd):/workspace map2check-dev:aflpp bash -c ' + cd /workspace/build_aflpp && ninja >/dev/null && ninja install >/dev/null && + cd /workspace && MAP2CHECK_PATH=/workspace/build_aflpp/install bash tests/integration/test_testcomp_regressions.sh 2>&1 | grep -E "FAIL|assert mode|refused|Results"' +``` +Expected: `PASS assert mode slices towards the assertions and still finds the violation`, `PASS --slice is refused where there is no criterion to slice towards`, and `Results: 22 passed, 0 failed`. + +- [ ] **Step 5: CHANGELOG** + +Add at the top of the unreleased section of `CHANGELOG.md`, following its existing format: + +```markdown +- tacasv2a: `--slice` no longer crashes KLEE and its test suites stay valid + on the original program. The slicer runs with `-cutoff-diverging=false` + (the cutoff's `exit(0)` had no debug location and KLEE rejected the + module), and every `__VERIFIER_nondet_*` function is a slicing criterion, + so the read order is preserved. `--slice` now also works with + `--check-asserts`. The slice is logged in functions/blocks/instructions. +``` + +- [ ] **Step 6: Commit** + +```bash +git add modules/frontend/map2check.cpp tests/integration/test_testcomp_regressions.sh CHANGELOG.md +git commit -m "feat(tacasv2a): --slice in assert mode + +Co-Authored-By: Claude Opus 5.5 (1M context) " +``` + +--- + +### Task 4: Validation on the diagnostic sample and the CI gates + +**Files:** none changed (verification only). If a check fails, fix it in the task that owns the code and re-run. + +**Interfaces:** +- Consumes: the full build from Tasks 1-3. + +- [ ] **Step 1: Re-run the 12-task diagnostic sample on the finished build** + +The manifest is the one from the spec's §2 (the 12 programs listed there, TSV columns `category program data_model expected_unreach`). Run both arms with the same build, `BUDGET=300 TESTCOV_S=300`, with `tests/testcomp/run_testcomp_evaluation.sh` (`PROPERTY=cover-error`, `EXTRA_FLAGS=""` for control and `EXTRA_FLAGS="--slice"` for the slice arm, `RESULTS_DIR` outside the repository). The container needs `python3-pip zip gcc gcc-multilib lcov` and `pip3 install testcov`. +Expected: the slice arm covers at least 10/12, and `ntdrivers/floppy.i.cil-1.c` is `FAILED,COVERED`. + +- [ ] **Step 2: Run the CI's TestCov step in the dev image** + +```bash +docker run --rm -u root -v $(pwd):/workspace -w /workspace -e MAP2CHECK_PATH=/workspace/build_aflpp/install map2check-dev:aflpp bash -c ' + apt-get update -qq && apt-get install -y -qq python3-pip zip gcc lcov >/dev/null && pip3 install --quiet testcov && + python3 tests/integration/test_benchexec_toolinfo.py 2>&1 | grep Results && + bash tests/integration/test_cover_branches.sh 2>&1 | grep Results && + bash tests/testcomp/run_testcov_suite.sh 2>&1 | grep -E "FAIL|Results"' +``` +Expected: `16 passed`, `5 passed`, `6 passed, 0 failed`. + +- [ ] **Step 3: Record the result** + +Append the sample table to the spec's §2 as "after implementation", then commit: + +```bash +git add docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md +git commit -m "docs(tacasv2a): diagnostic sample re-run on the implementation + +Co-Authored-By: Claude Opus 5.5 (1M context) " +``` diff --git a/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md b/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md new file mode 100644 index 000000000..73e66b7f0 --- /dev/null +++ b/docs/superpowers/specs/2026-09-26-tacasv2a-slicing-reach-assert-design.md @@ -0,0 +1,173 @@ +# tacasv2a — Slicing para reachability e assert que preserva a suíte de testes + +**Data:** 2026-09-26 +**Branch:** `tacas/slicing` (a partir de `tacas/aflpp`) +**Baseline:** tacasv1 (AFL++ 4.40c + CmpLog), mesmo motor com e sem `--slice` +**Status:** rascunho — aguardando revisão + +--- + +## 1. Objetivo + +Fazer o `--slice` deixar de **prejudicar** o Cover-Error e, se possível, ajudar. Na v15, o +braço com slice cobriu 412 tarefas contra 470 do controle (McNemar χ² = 36,10), com 57 +das 58 perdas em ECA. Esta etapa corrige a causa dessas perdas e estende o slicing ao +modo assert. É o primeiro sub-projeto da tacasv2 ("slicing por propriedade"); memória e +overflow ficam para 2b e 2c. + +> Linha de desenvolvimento: `decisions/tacas-afl-slicing-roadmap.md` (ai-memory). +> A tacasv2 parte da tacasv1 porque o AFL++ é a evolução decidida: nada é calibrado +> contra o LibFuzzer. + +--- + +## 2. Diagnóstico (medido em 2026-09-26) + +Amostra: 12 tarefas que a v15 cobria sem slice e perdia com slice (9 ECA, 3 de outras +famílias). Build tacasv1, orçamento de 300 s, TestCov 300 s, uma execução por braço. + +| braço | cobertas | +|---|---| +| controle (sem slice) | 11/12 | +| slice como está hoje | 6/12 | +| slice com `-cutoff-diverging=false` | 10/12 | +| slice sem cutoff + nondets como critério | 10/12 (e o único que cobre `floppy.i.cil-1`) | + +As duas tarefas que a última variante não cobriu terminaram perto do orçamento (~258 s). +Com uma execução por braço, não dá para separar isso de variação. + +**Depois da implementação** (2026-09-27, build final da `tacas/slicing`, mesma amostra e +orçamento, uma execução por braço): controle **12/12**, slice **12/12**. `floppy.i.cil-1` +dá FAILED + COVERED com slice. O slice terminou antes do controle em 5 das 9 tarefas ECA +(por exemplo, `Problem17_label55`: FAILED em 51 s, contra UNKNOWN em 137 s no controle). +São 12 tarefas: é validação de que os defeitos sumiram, não avaliação (§7). + +### Defeito 1 — o KLEE aborta em toda fatia com caminho cortado + +- O `--cutoff-diverging` (default `true` no dg/sbt-slicer) insere um bloco `diverge:` + com `call exit(0)` + `unreachable`. O `--help` diz "abort()", mas o código + (`dg/tools/llvm-slicer-preprocess.cpp`) chama `exit(0)`. +- Essas chamadas não têm localização de debug (`!dbg`), e o programa é compilado com `-g`. +- Quando o KLEE linka a uClibc, `exit` passa a ter corpo e o verificador rejeita o módulo: + `inlinable function call in a function with debug info must have a !dbg location` → + `LLVM ERROR: Broken module found`. O KLEE aborta (status 134) antes de executar. +- Em `eca-rers2012/Problem15_label09.c`, a fatia tem 60 blocos `diverge`. +- **Consequência:** no braço com slice da v15, o KLEE não rodou em nenhuma tarefa com + caminho cortado. Com o LibFuzzer, o `exit(0)` também encerrava a sessão de fuzzing. +- Com `-cutoff-diverging=false`, o KLEE da mesma tarefa roda até o fim (saída 0). + +### Defeito 2 — o vetor da fatia não vale no programa original + +- O slicer remove chamadas `__VERIFIER_nondet_*` cujo valor não afeta o critério. Em + `ntdrivers/floppy.i.cil-1.c`: 29 chamadas no programa, 10 na fatia. +- O vetor de entradas é gerado na fatia, mas o TestCov executa o **programa original**, + que consome mais valores e em outra ordem. O veredito sai FAILED e a suíte não cobre. +- Passar as funções nondet como critério **primário**, junto com o alvo, preserva as + chamadas alcançáveis: `floppy` passa a FAILED + COVERED. + +--- + +## 3. Decisões + +| Decisão | Valor | +|---|---| +| Cutoff | `-cutoff-diverging=false` | +| Critério em reachability | `` + todas as funções `__VERIFIER_nondet_*` conhecidas | +| Critério em assert | `__VERIFIER_assert` + as mesmas funções nondet | +| Onde fatiar | continua **antes** da instrumentação (`sliceWithRespectToTarget`, antes de `callPass`) | +| Stub da função alvo | mantém o stub `weak` atual | +| Visibilidade | `--statistics` no slicer; o Caller registra funções/blocos/instruções antes → depois | +| Outras flags (`--pta`, `--cda`, `--undefined-funs`) | defaults nesta etapa; calibrar só com medição própria | +| Cutoff "consertado" (manter o corte, corrigir `!dbg`, trocar `exit` por poda silenciosa) | fora; experimento condicional se a medição mostrar falta de eficiência de busca | + +A lista de funções nondet é fixa: as 16 que o `NonDetPass` instrumenta (`bool`, `char`, +`uchar`, `short`, `ushort`, `int`, `uint`, `unsigned`, `long`, `ulong`, `size_t`, +`loff_t`, `sector_t`, `pointer`, `pchar`, `double`) mais as do SV-COMP que ele ainda não +cobre (`float`, `longlong`, `ulonglong`, `_Bool`, `u8`, `u16`, `u32`, `charp`). O slicer +aceita nomes que não existem no programa. Isso foi verificado: não dá erro e não muda a +saída. Uma lista fixa dispensa desmontar o bitcode. + +--- + +## 4. Referência comparada: o que o Symbiotic faz + +Levantado no código do Symbiotic (master `4474bb9`), do sbt-slicer (`e350116`, o mesmo +SHA que o nosso Dockerfile fixa) e do dg. + +| Aspecto | Symbiotic | tacasv2a | Por quê | +|---|---|---|---| +| Fatia em Test-Comp (coverage-error/branches) | **Não** no pipeline principal | Sim, em Cover-Error | É onde o Map2Check usa o slicing; exige resolver o Defeito 2, que ele nunca enfrenta | +| `--cutoff-diverging` | Mantém (default) | Desliga | O KLEE dele reconhece violação por `-error-fn` e o módulo dele não quebra; o nosso quebra (Defeito 1) | +| Ponto do pipeline | Depois da instrumentação, com marcadores como critério | Antes da instrumentação | Para reach/assert o critério já existe no programa; os marcadores entram no 2b/2c | +| Contraexemplo | Reexecutado no programa sem slice (`-replay-nondets`) | Nondets preservados na fatia | Replay exigiria nomear cada nondet por call site; preservar é mais simples e resolve para Test-Comp | +| Flags extras | `-pta fi`, `-2c __VERIFIER_assume,klee_assume` (implícito) | Iguais por default | — | + +**O que é contribuição nossa:** slicing que **preserva a ordem de consumo das entradas**, de +modo que a suíte gerada na fatia continua válida no programa original. O Symbiotic não +precisa disso porque não gera suíte a partir da fatia. + +--- + +## 5. Mudanças + +### 5.1 `Caller::sliceWithRespectToTarget` (`modules/frontend/caller.cpp`) +- Recebe a lista de critérios em vez de só o nome da função alvo, e monta + `-c ,`. +- Acrescenta `-cutoff-diverging=false` e `--statistics`. +- Extrai do `slicer.output` as linhas `Statistics before/after` e registra + `Sliced with respect to X: F/B/I functions/blocks/instructions → F'/B'/I'`, mantendo + também os bytes. +- O restante (orçamento, fallback para o programa inteiro, stub `weak`) não muda. + +### 5.2 Gating em `map2check.cpp` +- `--slice` passa a valer também em `ASSERT_MODE`, com o critério `__VERIFIER_assert`. + Os demais modos continuam recusados com aviso, até o 2b e o 2c. + +### 5.3 Funções puras do slicing +- `modules/frontend/utils/slicer.hpp` (header-only, testável sem build completo): + `nondetFunctionNames()`, `slicingCriteria()`, `targetStubSource()` (o stub de + `__VERIFIER_assert` recebe `int cond`), `parseSlicerStatistics()` e `describeSlice()`. +- Em assert o critério primário é `__VERIFIER_assert,__assert_fail`: o `AssertPass` + instrumenta as duas. + +--- + +## 6. Testes + +Integração (`tests/integration/test_testcomp_regressions.sh`, seção de slicing): +1. **O KLEE sobrevive à fatia.** Um programa com ramos que não alcançam o alvo, rodado com + `--slice --nondet-generator symex`: sem `Broken module`, com FAILED. +2. **O vetor vale no original.** Um programa com um nondet irrelevante antes do relevante + (`int a = nondet(); int b = nondet(); if (b == 42) reach_error();`), rodado com + `--slice --generate-test-suite`: a suíte tem 2 entradas, na ordem do original. +3. **Assert fatia.** `--check-asserts --slice` registra `Sliced with respect to + __VERIFIER_assert` e mantém o veredito. +4. Os testes existentes de slicing ("degrade loudly", recusa em cover-branches) continuam. + +Unitário: se a extração das estatísticas virar função própria, um teste de parser sobre um +`slicer.output` fixo. + +--- + +## 7. Avaliação (tacasv2a) + +- **Quando:** depois do merge do PR #66 e desta branch, na execução sequencial combinada + com o usuário. +- **Como:** corpus de Cover-Error (1087 tarefas pareadas, `cover-error-q400.tsv`), dois + braços com o **mesmo build**: controle (sem slice) e `--slice`. Orçamento de 300 s, + 3 shards, como na v15. +- **Critério de sucesso:** o braço com slice **não perde** para o controle (McNemar sem + diferença significativa contra, ou a favor) e as perdas em ECA desaparecem. +- **Relato:** cobertas por família, perdas/ganhos pareados e estatísticas de redução + (instruções antes/depois). + +--- + +## 8. Riscos + +| Risco | Mitigação | +|---|---| +| Sem o cutoff, a fatia fica maior e o ganho de busca diminui | É o preço da correção. O cutoff "consertado" fica como experimento condicional (§3) | +| Preservar nondets puxa código que a fatia removeria | Medido no `floppy`: 8933 → 9155 linhas de IR (+2,5%). Acompanhar a redução na avaliação | +| Alguma função nondet fora da lista | A lista inclui as do SV-COMP; uma função ausente só reproduz o Defeito 2 naquela tarefa, e o teste 2 detecta o caso comum | +| Amostra de 12 tarefas | É diagnóstico, não avaliação; a conclusão vem da §7 | diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index d6584a0f8..5e64ec14b 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -22,6 +22,7 @@ #include #include #include +#include #include #include #include @@ -30,6 +31,7 @@ #include "test_suite/ktest_reader.hpp" #include "utils/gen_crypto_hash.hpp" #include "utils/log.hpp" +#include "utils/slicer.hpp" #include "utils/tools.hpp" // namespace fs = boost::filesystem; // } // namespace @@ -176,7 +178,8 @@ std::string Caller::exportFuzzerVectorAsKtest() { return path; } -bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { +bool Caller::sliceWithRespectToTarget(const std::string &targetFunction, + const std::vector &criteria) { const std::string slicer = Map2Check::slicerBinary(); if (!std::filesystem::exists(slicer)) { // Announced, not silently skipped. A slicer that is asked for and absent @@ -218,10 +221,37 @@ bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { 1.0, std::min(0.2 * this->timeout, std::max(1.0, static_cast(remainingSeconds()) - 5.0))); - command << "timeout -k " << Map2Check::killGracePeriod << " " << static_cast(sliceBudget) - << " " << slicer << " -c " << targetFunction - << " --entry=main -o " << output << " " - << input << " > slicer.output 2>&1"; + // -cutoff-diverging=false: the cutoff rewrites every path that cannot reach + // the criterion into exit(0) with no debug location, and once KLEE links + // uClibc the verifier rejects the module ("Broken module found") -- KLEE + // never ran on a sliced task with a cut path (tacasv2a spec, defect 1). + // + // The nondet functions ride along as criteria so that every read the + // original program performs survives; the suite is generated on the slice + // and replayed on the original (defect 2). + // + // --statistics: counts before and after, logged below. + // The program's own nondet names join the fixed list: no fixed list knows + // every name a benchmark declares, and a missing one silently shifts the + // suite again. Read from the textual IR -- the bitcode string table packs + // names with no separator. If the disassembly fails, the fixed list stands. + const std::string inputIR = programHash + "-slice-input.ll"; + std::ostringstream disassemble; + disassemble << Map2Check::optBinary << " -S " << input << " -o " << inputIR + << " > /dev/null 2>&1"; + std::vector programNondets; + if (system(disassemble.str().c_str()) == 0) { + std::ifstream irFile(inputIR); + std::stringstream irText; + irText << irFile.rdbuf(); + programNondets = Map2Check::nondetNamesInIR(irText.str()); + } + + command << "timeout -k " << Map2Check::killGracePeriod << " " + << static_cast(sliceBudget) << " " << slicer << " -c " + << Map2Check::slicingCriteria(criteria, programNondets) + << " --entry=main -cutoff-diverging=false --statistics -o " << output + << " " << input << " > slicer.output 2>&1"; Map2Check::Log::Debug(command.str()); const int result = system(command.str().c_str()); @@ -240,9 +270,16 @@ bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { // of how much was dropped. const auto before = std::filesystem::file_size(input, error); const auto after = std::filesystem::file_size(output, error); - Map2Check::Log::Info("Sliced with respect to " + targetFunction + ": " + - std::to_string(before) + " -> " + - std::to_string(after) + " bytes of bitcode"); + std::ifstream slicerLog("slicer.output"); + std::stringstream slicerText; + slicerText << slicerLog.rdbuf(); + std::string criterionLabel; + for (const std::string &name : criteria) { + criterionLabel += (criterionLabel.empty() ? "" : ",") + name; + } + Map2Check::Log::Info(Map2Check::describeSlice( + criterionLabel, Map2Check::parseSlicerStatistics(slicerText.str()), + before, after)); // sbt-slicer removes the body of the criterion function itself. reach_error // is where the slice ENDS -- nothing it does can influence whether it is @@ -266,7 +303,7 @@ bool Caller::sliceWithRespectToTarget(const std::string &targetFunction) { { std::ofstream stub(stubSource); if (stub.is_open()) { - stub << "void __attribute__((weak)) " << targetFunction << "(void) {}\n"; + stub << Map2Check::targetStubSource(targetFunction); } } std::ostringstream compileStub; diff --git a/modules/frontend/caller.hpp b/modules/frontend/caller.hpp index 7119d0699..0c8675034 100644 --- a/modules/frontend/caller.hpp +++ b/modules/frontend/caller.hpp @@ -130,10 +130,17 @@ class Caller { * decision the caller makes rather than a default. */ bool sliceProgram = false; - /** Runs sbt-slicer over the instrumented bitcode. Returns false if the - * slicer is unavailable or produced nothing usable, leaving the original - * bitcode in place. */ - bool sliceWithRespectToTarget(const std::string& targetFunction); + /** Runs sbt-slicer over the compiled (not yet instrumented) bitcode. + * + * `criteria` are the primary slicing criteria (the target function, or the + * assert functions); every __VERIFIER_nondet_* function is added to them so + * the suite found on the slice stays valid on the original program. The + * cutoff of diverging paths is off: its exit(0) carries no debug location + * and KLEE rejects the module. `targetFunction` gets its body back through a + * weak stub. Returns false if the slicer is unavailable or produced nothing + * usable, leaving the original bitcode in place. */ + bool sliceWithRespectToTarget(const std::string& targetFunction, + const std::vector& criteria); /** Turns on the exchange of input vectors between the two engines. * diff --git a/modules/frontend/map2check.cpp b/modules/frontend/map2check.cpp index cd5e7f91e..48858ecad 100644 --- a/modules/frontend/map2check.cpp +++ b/modules/frontend/map2check.cpp @@ -514,16 +514,22 @@ int map2check_execution(map2check_args args) { // properties: the search space is smaller and the instrumentation is added // to what survives. // - // Reachability only. Slicing needs a criterion, and Cover-Branches has none - // -- every branch is the goal. Asking elsewhere is refused, not ignored. + // Reachability and assert. Slicing needs a criterion, and Cover-Branches has + // none -- every branch is the goal. Asking elsewhere is refused, not ignored. + // Reachability slices towards the target; assert towards the two functions + // AssertPass instruments. Memory properties and overflow need their own + // criteria (tacasv2b/2c). if (args.sliceProgram) { if (args.mode == Map2Check::Map2CheckMode::REACHABILITY_MODE) { - caller->sliceWithRespectToTarget(args.function); + caller->sliceWithRespectToTarget(args.function, {args.function}); + } else if (args.mode == Map2Check::Map2CheckMode::ASSERT_MODE) { + caller->sliceWithRespectToTarget("__VERIFIER_assert", + {"__VERIFIER_assert", "__assert_fail"}); } else { Map2Check::Log::Warning( - "--slice applies to reachability only: there is no criterion to " - "slice towards when the goal is coverage or a memory property. " - "Analysing the whole program."); + "--slice applies to reachability and assert only: there is no " + "criterion to slice towards when the goal is coverage or a memory " + "or overflow property. Analysing the whole program."); } } @@ -751,8 +757,9 @@ z3 (Z3 is default), btor (Boolector), and yices2 (Yices))") ("test-suite-dir", po::value()->default_value("test-suite"), "\tdirectory to write the test suite into") ("slice", - "\tslice the program with respect to the target before analysing it " - "(reachability only; needs sbt-slicer)") + "\tslice the program with respect to the target (reachability) or " + "the assertions (--check-asserts) before analysing it; needs " + "sbt-slicer") ("seed-exchange", "\tlet the two engines hand each other input vectors through a shared " "seed corpus (hybrid runs; off by default)") diff --git a/modules/frontend/utils/slicer.hpp b/modules/frontend/utils/slicer.hpp new file mode 100644 index 000000000..c96b91cf6 --- /dev/null +++ b/modules/frontend/utils/slicer.hpp @@ -0,0 +1,163 @@ +/** + * Copyright (C) 2014 - 2026 Map2Check tool + * This file is part of the Map2Check tool, and is made available under + * the terms of the GNU General Public License version 2. + * + * SPDX-License-Identifier: (GPL-2.0) + **/ + +#ifndef MODULES_FRONTEND_UTILS_SLICER_HPP_ +#define MODULES_FRONTEND_UTILS_SLICER_HPP_ + +#include +#include +#include +#include +#include +#include + +namespace Map2Check { + +/** Every __VERIFIER_nondet_* function the slice must keep. + * + * The suite is generated on the slice, but TestCov runs it on the ORIGINAL + * program. A nondet call the slicer drops -- its value does not reach the + * criterion -- is still consumed by the original, so the vector shifts and + * the suite stops covering (measured: ntdrivers/floppy.i.cil-1.c, 29 reads in + * the program and 10 in the slice; FAILED, NOT_COVERED). Keeping these calls + * as criteria keeps the consumption order. + * + * The first sixteen are what NonDetPass instruments; the rest are SV-COMP + * names it does not model yet, kept so their order is not lost either. The + * slicer accepts names the program does not use. */ +inline const std::vector& nondetFunctionNames() { + static const std::vector names = { + "__VERIFIER_nondet_bool", "__VERIFIER_nondet_char", + "__VERIFIER_nondet_uchar", "__VERIFIER_nondet_short", + "__VERIFIER_nondet_ushort", "__VERIFIER_nondet_int", + "__VERIFIER_nondet_uint", "__VERIFIER_nondet_unsigned", + "__VERIFIER_nondet_long", "__VERIFIER_nondet_ulong", + "__VERIFIER_nondet_size_t", "__VERIFIER_nondet_loff_t", + "__VERIFIER_nondet_sector_t", "__VERIFIER_nondet_pointer", + "__VERIFIER_nondet_pchar", "__VERIFIER_nondet_double", + "__VERIFIER_nondet_float", "__VERIFIER_nondet_longlong", + "__VERIFIER_nondet_ulonglong", "__VERIFIER_nondet__Bool", + "__VERIFIER_nondet_u8", "__VERIFIER_nondet_u16", + "__VERIFIER_nondet_u32", "__VERIFIER_nondet_charp"}; + return names; +} + +/** Every __VERIFIER_nondet_* symbol in a module's textual IR (`opt -S`), + * in order of first appearance. The fixed list above cannot know every name a + * benchmark declares (int128, uint128, ...), and a name missing from the + * criteria silently brings the shifted suite back. */ +inline std::vector nondetNamesInIR(const std::string& ir) { + static const std::regex symbol(R"(@(__VERIFIER_nondet_[A-Za-z0-9_]+))"); + std::vector names; + for (std::sregex_iterator it(ir.begin(), ir.end(), symbol), end; it != end; + ++it) { + const std::string name = (*it)[1]; + if (std::find(names.begin(), names.end(), name) == names.end()) { + names.push_back(name); + } + } + return names; +} + +/** The -c argument: the primary criteria, then every nondet function -- the + * fixed list plus `fromProgram` (nondetNamesInIR), each name once. */ +inline std::string slicingCriteria( + const std::vector& primary, + const std::vector& fromProgram = {}) { + std::vector all(primary); + auto add = [&all](const std::string& name) { + if (std::find(all.begin(), all.end(), name) == all.end()) { + all.push_back(name); + } + }; + for (const std::string& name : nondetFunctionNames()) add(name); + for (const std::string& name : fromProgram) add(name); + std::ostringstream criteria; + for (size_t i = 0; i < all.size(); ++i) { + criteria << (i == 0 ? "" : ",") << all[i]; + } + return criteria.str(); +} + +/** A weak definition of the criterion function, restoring the body the + * slicer removes without displacing a real one. The signature must match + * the program's declaration, or llvm-link rejects the module. */ +inline std::string targetStubSource(const std::string& function) { + if (function == "__VERIFIER_assert") { + return "void __attribute__((weak)) __VERIFIER_assert(int cond) {}\n"; + } + return "void __attribute__((weak)) " + function + "(void) {}\n"; +} + +struct SlicerCounts { + unsigned globals = 0; + unsigned functions = 0; + unsigned blocks = 0; + unsigned instructions = 0; +}; + +struct SlicerStatistics { + bool found = false; // both the "before" and the "after" line were read + SlicerCounts before; + SlicerCounts after; +}; + +/** Reads sbt-slicer's --statistics lines: + * Statistics before Globals/Functions/Blocks/Instr.: 37 97 2215 10764 + * Statistics after Globals/Functions/Blocks/Instr.: 37 38 444 2989 */ +inline SlicerStatistics parseSlicerStatistics(const std::string& slicerOutput) { + static const std::regex line( + R"(Statistics (before|after) Globals/Functions/Blocks/Instr\.:\s+)" + R"((\d+)\s+(\d+)\s+(\d+)\s+(\d+))"); + SlicerStatistics stats; + bool sawBefore = false; + bool sawAfter = false; + for (std::sregex_iterator it(slicerOutput.begin(), slicerOutput.end(), line), + end; + it != end; ++it) { + const std::smatch& m = *it; + SlicerCounts counts; + counts.globals = static_cast(std::stoul(m[2])); + counts.functions = static_cast(std::stoul(m[3])); + counts.blocks = static_cast(std::stoul(m[4])); + counts.instructions = static_cast(std::stoul(m[5])); + if (m[1] == "before") { + stats.before = counts; + sawBefore = true; + } else { + stats.after = counts; + sawAfter = true; + } + } + stats.found = sawBefore && sawAfter; + return stats; +} + +/** The one log line a slice produces. Counts when the slicer reported them, + * bytes always -- a slice narrows the question being answered, and this line + * is the only visible sign of how much was dropped. */ +inline std::string describeSlice(const std::string& criterion, + const SlicerStatistics& stats, + uintmax_t bytesBefore, uintmax_t bytesAfter) { + std::ostringstream text; + text << "Sliced with respect to " << criterion << ": "; + if (stats.found) { + text << stats.before.functions << "/" << stats.before.blocks << "/" + << stats.before.instructions << " -> " << stats.after.functions << "/" + << stats.after.blocks << "/" << stats.after.instructions + << " functions/blocks/instructions (" << bytesBefore << " -> " + << bytesAfter << " bytes of bitcode)"; + } else { + text << bytesBefore << " -> " << bytesAfter << " bytes of bitcode"; + } + return text.str(); +} + +} // namespace Map2Check + +#endif // MODULES_FRONTEND_UTILS_SLICER_HPP_ diff --git a/tests/integration/test_testcomp_regressions.sh b/tests/integration/test_testcomp_regressions.sh index d3b187fa9..74789b97d 100755 --- a/tests/integration/test_testcomp_regressions.sh +++ b/tests/integration/test_testcomp_regressions.sh @@ -516,12 +516,140 @@ fi ( cd "$WORK/slice" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ --memtrack --slice --nondet-generator symex --timeout 45 reach.c ) \ > "$WORK/slice/mode.log" 2>&1 -if grep -q "applies to reachability only" "$WORK/slice/mode.log"; then +if grep -q "applies to reachability and assert only" "$WORK/slice/mode.log"; then ok "--slice is refused where there is no criterion to slice towards" else fail "slice mode guard" "--slice was accepted in a mode that has no criterion" fi +# --- 13. a slice must leave KLEE something it can run ------------------------- +# sbt-slicer's --cutoff-diverging (default on) rewrites every path that cannot +# reach the criterion into a `diverge:` block calling exit(0) -- with no debug +# location. The program is compiled with -g; once KLEE links uClibc, exit has a +# body, and the verifier rejects the module ("inlinable function call in a +# function with debug info must have a !dbg location"). KLEE aborted before +# executing anything, on every sliced task with a cut path: the slice arm of +# the v15 campaign ran without its symbolic engine. +mkdir -p "$WORK/cut" +# ECA-shaped on purpose: the slicer turns a plain return from main into a +# `safe_return`, so a straight-line program never gets a `diverge:` block. A +# reactive loop whose step can take a path that never reaches the target does; +# bounded to two steps so that KLEE decides it well inside the budget. +cat > "$WORK/cut/cut.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void reach_error(void); +extern void exit(int); +int a = 1; +void step(int in) { + if (in == 5) { a = 2; return; } + if (in == 6 && a == 2) { reach_error(); } + if (in == 9) { exit(0); } +} +int main(void) { + for (int i = 0; i < 2; i++) { + int in = __VERIFIER_nondet_int(); + step(in); + } + return 0; +} +EOF +( cd "$WORK/cut" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --slice \ + --nondet-generator symex --timeout 45 cut.c ) > "$WORK/cut/run.log" 2>&1 +if grep -q "Broken module" "$WORK/cut/run.log"; then + fail "slice + KLEE" "KLEE rejected the sliced module (cutoff exit without !dbg)" +elif grep -q "VERIFICATION FAILED" "$WORK/cut/run.log"; then + ok "KLEE runs on the slice and reaches the target" +else + fail "slice + KLEE" "no FAILED verdict on a trivially reachable target" + grep -E "Sliced|Exited klee|VERIFICATION" "$WORK/cut/run.log" | sed 's/^/ /' +fi + +# --- 14. a suite found on the slice must hold on the original ---------------- +# TestCov runs the suite on the ORIGINAL program. A nondet read the slicer +# dropped -- its value does not reach the target -- is still consumed there, +# so the vector shifts: measured on ntdrivers/floppy.i.cil-1.c, FAILED and +# NOT_COVERED. The slice keeps every nondet call, so both values appear, in +# the original order. +mkdir -p "$WORK/order" +cp "$WORK/one/reach.prp" "$WORK/order/" +cat > "$WORK/order/order.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void reach_error(void); +int main(void) { + int a = __VERIFIER_nondet_int(); + int b = __VERIFIER_nondet_int(); + if (b == 42) { reach_error(); } + return a; +} +EOF +( cd "$WORK/order" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --slice \ + --nondet-generator symex --generate-test-suite --property-file reach.prp \ + --timeout 60 order.c ) > "$WORK/order/run.log" 2>&1 +order_inputs=$(sed -n 's:.*\(.*\).*:\1:p' \ + "$WORK/order/test-suite/testcase-1.xml" 2>/dev/null | tr '\n' ' ') +if [ "$(echo $order_inputs | wc -w)" -eq 2 ] && \ + [ "$(echo $order_inputs | awk '{print $2}')" = "42" ]; then + ok "the sliced suite keeps the original read order [$order_inputs]" +else + fail "slice read order" "expected 2 inputs ending in 42, got [$order_inputs]" +fi + +# --- 15. assert mode slices towards the assertions ---------------------------- +# AssertPass instruments __VERIFIER_assert and __assert_fail, so those are the +# criteria. The program only DECLARES __VERIFIER_assert: the weak stub must +# take the condition, or llvm-link rejects the (void) definition. +mkdir -p "$WORK/assert" +cat > "$WORK/assert/assert.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern void __VERIFIER_assert(int cond); +int main(void) { + int a = __VERIFIER_nondet_int(); + int b = __VERIFIER_nondet_int(); + if (a > 0) { a = a - 1; } + __VERIFIER_assert(b != 77); + return a; +} +EOF +( cd "$WORK/assert" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --check-asserts --slice --nondet-generator symex --timeout 45 assert.c ) \ + > "$WORK/assert/run.log" 2>&1 +if grep -q "Sliced with respect to __VERIFIER_assert,__assert_fail" "$WORK/assert/run.log" && \ + grep -q "VERIFICATION FAILED" "$WORK/assert/run.log"; then + ok "assert mode slices towards the assertions and still finds the violation" +else + fail "assert slice" "no assert-criterion slice, or the violation was lost" + grep -E "Sliced|slice|VERIFICATION" "$WORK/assert/run.log" | sed 's/^/ /' +fi + +# --- 16. nondet names the fixed list does not know are kept too -------------- +# The criteria carry a fixed list of __VERIFIER_nondet_* names, and no fixed +# list knows every name a benchmark declares (int128, uint128, ...). A missing +# one silently brings back the shifted suite of section 14, so the names are +# also read from the program. Checked on the slicer command itself: int128 is +# not in the fixed list, so its presence there proves it came from the program. +mkdir -p "$WORK/names" +cat > "$WORK/names/names.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +extern __int128 __VERIFIER_nondet_int128(void); +extern void reach_error(void); +int main(void) { + __int128 wide = __VERIFIER_nondet_int128(); + int b = __VERIFIER_nondet_int(); + if (b == 42) { reach_error(); } + return (int)wide; +} +EOF +( cd "$WORK/names" && MAP2CHECK_PATH="$MAP2CHECK_DIR" timeout -k 10 200 "$MAP2CHECK" \ + --target-function --target-function-name reach_error --slice --debug \ + --nondet-generator symex --timeout 30 names.c ) > "$WORK/names/run.log" 2>&1 +if grep "sbt-slicer" "$WORK/names/run.log" | grep -q "__VERIFIER_nondet_int128"; then + ok "nondet names declared by the program are slicing criteria too" +else + fail "program nondet names" "__VERIFIER_nondet_int128 is not among the criteria" +fi + echo " ---" echo " Results: $PASSED passed, $FAILED failed" [ "$FAILED" -eq 0 ] || exit 1 diff --git a/tests/unit/frontend/CMakeLists.txt b/tests/unit/frontend/CMakeLists.txt index c4ecc97f0..35d6a0390 100644 --- a/tests/unit/frontend/CMakeLists.txt +++ b/tests/unit/frontend/CMakeLists.txt @@ -15,3 +15,8 @@ add_executable(KtestReaderTest $ ) map2check_test(KtestReaderTest) + +add_executable(SlicerTest + SlicerTest.cpp +) +map2check_test(SlicerTest) diff --git a/tests/unit/frontend/SlicerTest.cpp b/tests/unit/frontend/SlicerTest.cpp new file mode 100644 index 000000000..9a312b809 --- /dev/null +++ b/tests/unit/frontend/SlicerTest.cpp @@ -0,0 +1,124 @@ +/** + * Copyright (C) 2014 - 2026 Map2Check tool + * This file is part of the Map2Check tool, and is made available under + * the terms of the GNU General Public License version 2. + * + * SPDX-License-Identifier: (GPL-2.0) + **/ + +#include + +#include +#include +#include + +#include "../../../modules/frontend/utils/slicer.hpp" + +// The suite is generated on the slice and run by TestCov on the ORIGINAL +// program, so every nondet read the original performs must survive slicing. +TEST(SlicingCriteria, AppendsEveryNondetFunctionAfterThePrimary) { + const std::string criteria = Map2Check::slicingCriteria({"reach_error"}); + EXPECT_EQ(criteria.rfind("reach_error,", 0), 0u); + for (const std::string& name : Map2Check::nondetFunctionNames()) { + EXPECT_NE(criteria.find("," + name), std::string::npos) << name; + } +} + +TEST(SlicingCriteria, KeepsSeveralPrimariesInOrder) { + const std::string criteria = + Map2Check::slicingCriteria({"__VERIFIER_assert", "__assert_fail"}); + EXPECT_EQ(criteria.rfind("__VERIFIER_assert,__assert_fail,", 0), 0u); +} + +TEST(NondetFunctionNames, CoversWhatNonDetPassInstruments) { + const auto& names = Map2Check::nondetFunctionNames(); + for (const char* type : {"bool", "char", "uchar", "short", "ushort", "int", + "uint", "unsigned", "long", "ulong", "size_t", + "loff_t", "sector_t", "pointer", "pchar", "double"}) { + const std::string name = std::string("__VERIFIER_nondet_") + type; + EXPECT_NE(std::find(names.begin(), names.end(), name), names.end()) << name; + } +} + +TEST(TargetStubSource, VoidTargetGetsAVoidStub) { + EXPECT_EQ(Map2Check::targetStubSource("reach_error"), + "void __attribute__((weak)) reach_error(void) {}\n"); +} + +// __VERIFIER_assert takes the condition; a (void) stub would not link against +// the program's own declaration. +TEST(TargetStubSource, AssertStubTakesTheCondition) { + EXPECT_EQ(Map2Check::targetStubSource("__VERIFIER_assert"), + "void __attribute__((weak)) __VERIFIER_assert(int cond) {}\n"); +} + +TEST(ParseSlicerStatistics, ReadsBeforeAndAfter) { + const std::string output = + "Statistics before Globals/Functions/Blocks/Instr.: 37 97 2215 10764\n" + "[llvm-slicer] Sliced away 1454 from 4227 nodes in DG\n" + "Statistics after Globals/Functions/Blocks/Instr.: 37 38 444 2989\n"; + const Map2Check::SlicerStatistics stats = + Map2Check::parseSlicerStatistics(output); + ASSERT_TRUE(stats.found); + EXPECT_EQ(stats.before.functions, 97u); + EXPECT_EQ(stats.before.blocks, 2215u); + EXPECT_EQ(stats.before.instructions, 10764u); + EXPECT_EQ(stats.after.globals, 37u); + EXPECT_EQ(stats.after.functions, 38u); + EXPECT_EQ(stats.after.instructions, 2989u); +} + +// A slicer that prints no statistics must not be reported as having sliced +// everything away. +TEST(ParseSlicerStatistics, MissingLinesAreNotFound) { + EXPECT_FALSE(Map2Check::parseSlicerStatistics("").found); + EXPECT_FALSE(Map2Check::parseSlicerStatistics( + "Statistics before Globals/Functions/Blocks/Instr.: 1 2 3 4\n") + .found); +} + +TEST(DescribeSlice, ReportsCountsWhenFound) { + Map2Check::SlicerStatistics stats; + stats.found = true; + stats.before = {37, 97, 2215, 10764}; + stats.after = {37, 38, 444, 2989}; + EXPECT_EQ(Map2Check::describeSlice("reach_error", stats, 184164, 171708), + "Sliced with respect to reach_error: 97/2215/10764 -> 38/444/2989 " + "functions/blocks/instructions (184164 -> 171708 bytes of " + "bitcode)"); +} + +TEST(DescribeSlice, FallsBackToBytesWithoutStatistics) { + EXPECT_EQ(Map2Check::describeSlice("reach_error", {}, 10, 8), + "Sliced with respect to reach_error: 10 -> 8 bytes of bitcode"); +} + +// The fixed list cannot know every name a benchmark declares (int128, +// uint128, ...); a name missing from the criteria silently reintroduces the +// shifted suite. The names come from the program itself as well. +TEST(NondetNamesInIR, FindsEveryDeclaredOrCalledNondetFunction) { + const std::string ir = + "declare i32 @__VERIFIER_nondet_int()\n" + "declare i128 @__VERIFIER_nondet_int128()\n" + " %1 = call i128 @__VERIFIER_nondet_int128(), !dbg !19\n" + " call void @reach_error()\n" + "@__VERIFIER_nondet_not_a_call = global i32 0\n"; + const std::vector names = Map2Check::nondetNamesInIR(ir); + ASSERT_EQ(names.size(), 3u); + EXPECT_EQ(names[0], "__VERIFIER_nondet_int"); + EXPECT_EQ(names[1], "__VERIFIER_nondet_int128"); + EXPECT_EQ(names[2], "__VERIFIER_nondet_not_a_call"); +} + +TEST(SlicingCriteria, AddsNamesFromTheProgramOnceEach) { + const std::string criteria = Map2Check::slicingCriteria( + {"reach_error"}, {"__VERIFIER_nondet_int128", "__VERIFIER_nondet_int"}); + EXPECT_NE(criteria.find(",__VERIFIER_nondet_int128"), std::string::npos); + size_t count = 0; + for (size_t at = criteria.find("__VERIFIER_nondet_int,"); + at != std::string::npos; + at = criteria.find("__VERIFIER_nondet_int,", at + 1)) { + ++count; + } + EXPECT_EQ(count, 1u); +}