From 5c40b38074975737a35597a7228cc83725a45f02 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 7 Nov 2026 03:38:06 -0400 Subject: [PATCH 1/7] fix(testcomp): keep the run below its cgroup memory limit The Test-Comp 2027 pre-run (900 s, 3 GB) ended 1,747 runs as OUT OF MEMORY. BenchExec enforces the limit on the whole run, tmpfs included, and none of the engines knew it: - 821 runs died in KLEE's seeding loop, which never checks --max-memory; - about 200 with KLEE at its fixed 2,000 MB cap plus the files in tmpfs; - 239 in the first fuzzer phase: afl-fuzz runs its target unlimited. Map2Check now reads the run's limit from the cgroup (memory.max, visible inside the BenchExec container; MAP2CHECK_MEMORY_LIMIT_MB overrides it): - KLEE's --max-memory is 40% of the limit, at most KLEE's default 2,000 MB, so a 15 GB run keeps the cap it had (MAP2CHECK_KLEE_MAX_MEMORY still wins); - the KLEE watchdog reads memory.current every half second, seeding included: SIGINT at 80% of the limit (KLEE halts and writes its tests), SIGKILL at 92%. A phase stopped this way counts as incomplete; - the afl-fuzz target (-m) and the native replays (ulimit -v) get a third of the limit. With no limit found, nothing changes. --- modules/frontend/caller.cpp | 170 ++++++++++++++++++----- modules/frontend/caller.hpp | 2 + modules/frontend/utils/memory_budget.hpp | 129 +++++++++++++++++ tests/unit/frontend/CMakeLists.txt | 5 + tests/unit/frontend/MemoryBudgetTest.cpp | 115 +++++++++++++++ 5 files changed, 385 insertions(+), 36 deletions(-) create mode 100644 modules/frontend/utils/memory_budget.hpp create mode 100644 tests/unit/frontend/MemoryBudgetTest.cpp diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index fa13681c4..eff9520b8 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -43,6 +43,7 @@ #include "utils/gen_crypto_hash.hpp" #include "utils/alternation.hpp" #include "utils/log.hpp" +#include "utils/memory_budget.hpp" #include "utils/seed_store.hpp" #include "utils/slicer.hpp" #include "utils/tools.hpp" @@ -170,6 +171,30 @@ std::string Caller::postOptimizationFlags() { return flags.str(); } +namespace { +/** The cgroup whose memory.max limits this run, found once (empty: none). */ +const std::string &runCgroup() { + static const std::string cgroup = Map2Check::limitingCgroup(); + return cgroup; +} + +/** The run's memory limit in MB, 0 when unknown (see memory_budget.hpp). */ +long long runLimitMB() { + static const long long limit = Map2Check::runMemoryLimitMB(runCgroup()); + return limit; +} + +/** A shell prefix that caps the address space of a program run natively at + * nativeMemoryLimitMB, or nothing when the run's limit is unknown. A replay + * that allocates past it fails its malloc instead of crossing the limit that + * ends the whole run. */ +std::string nativeMemoryPrefix() { + const long long megabytes = Map2Check::nativeMemoryLimitMB(runLimitMB()); + if (megabytes <= 0) return ""; + return "ulimit -v " + std::to_string(megabytes * 1024) + " 2>/dev/null; "; +} +} // namespace + namespace { /** KLEE's covered-instruction count, from the last row of the SQLite stats * database it rewrites every second; -1 when it cannot be read (not created @@ -249,10 +274,18 @@ std::string lastLines(const std::string &path, size_t count) { int Caller::runKleeWatched(const std::string &command) { this->stoppedOnStagnation = false; -#ifndef MAP2CHECK_HAVE_SQLITE - return system(command.c_str()); + this->stoppedForMemory = false; + // Two reasons to stop KLEE before its own deadline: no new coverage + // (needs the SQLite stats) and the run's memory, read from the cgroup + // BenchExec limits. Neither available: KLEE runs unwatched, as before. + const std::string &cgroup = runCgroup(); + const long long limitMB = runLimitMB(); +#ifdef MAP2CHECK_HAVE_SQLITE + const bool watchCoverage = this->stagnationLimit > 0; #else - if (this->stagnationLimit == 0) return system(command.c_str()); + const bool watchCoverage = false; +#endif + if (!watchCoverage && limitMB <= 0) return system(command.c_str()); // The shell's pid becomes the pid of `timeout` through exec, and `timeout` // forwards a SIGINT to KLEE -- whose handler halts the search cleanly and @@ -267,22 +300,10 @@ int Caller::runKleeWatched(const std::string &command) { done = true; }); - Map2Check::CoverageWatch watch(this->stagnationLimit); - const auto started = std::chrono::steady_clock::now(); - const std::string stats = std::string(Map2Check::kleeOutputDir) + "/run.stats"; - while (!done) { - for (int tick = 0; tick < 4 && !done; ++tick) { - std::this_thread::sleep_for(std::chrono::milliseconds(500)); - } - if (done) break; - const double now = std::chrono::duration( - std::chrono::steady_clock::now() - started) - .count(); - if (!watch.stagnated(kleeCoveredInstructions(stats), now)) continue; - - // To KLEE itself, the child of `timeout`: signalled, `timeout` forwards - // to the child AND its process group, KLEE gets two SIGINTs, and the - // second one exits before the halt dump of the live states is written. + // To KLEE itself, the child of `timeout`: signalled, `timeout` forwards + // to the child AND its process group, KLEE gets two SIGINTs, and the + // second one exits before the halt dump of the live states is written. + auto signalKlee = [](int signal) { pid_t pid = 0; std::ifstream("klee.pid") >> pid; pid_t klee = 0; @@ -292,30 +313,84 @@ int Caller::runKleeWatched(const std::string &command) { children >> klee; } if (klee > 0) { - kill(klee, SIGINT); + kill(klee, signal); } else if (pid > 0) { - kill(pid, SIGINT); + kill(pid, signal); + } + }; + // What the whole run uses now -- KLEE, the frontend and every file in the + // tmpfs -- against the limit BenchExec kills the whole run at. + auto memoryNow = [&cgroup, limitMB]() { + if (limitMB <= 0 || cgroup.empty()) return Map2Check::MemoryAction::None; + return Map2Check::memoryAction( + Map2Check::readCgroupBytes(cgroup + "/memory.current"), limitMB); + }; + auto killForMemory = [&]() { + signalKlee(SIGKILL); + this->stoppedForMemory = true; + Map2Check::Log::Warning( + "KLEE killed: the run reached 92% of its memory limit (" + + std::to_string(limitMB) + " MB)"); + }; + + Map2Check::CoverageWatch watch(this->stagnationLimit); + const auto started = std::chrono::steady_clock::now(); + const std::string stats = std::string(Map2Check::kleeOutputDir) + "/run.stats"; + while (!done) { + // Memory is read every half second: KLEE's seeding loop can add + // hundreds of MB in a second, and it never checks --max-memory itself. + Map2Check::MemoryAction memory = Map2Check::MemoryAction::None; + for (int tick = 0; tick < 4 && !done; ++tick) { + std::this_thread::sleep_for(std::chrono::milliseconds(500)); + memory = memoryNow(); + if (memory != Map2Check::MemoryAction::None) break; + } + if (done) break; + if (memory == Map2Check::MemoryAction::Kill) { + killForMemory(); + break; + } + bool stagnated = false; + if (memory == Map2Check::MemoryAction::None) { + if (!watchCoverage) continue; + const double now = std::chrono::duration( + std::chrono::steady_clock::now() - started) + .count(); + stagnated = watch.stagnated(kleeCoveredInstructions(stats), now); + if (!stagnated) continue; + } + + signalKlee(SIGINT); + if (stagnated) { + this->stoppedOnStagnation = true; + Map2Check::Log::Warning("KLEE stagnated: no new coverage for " + + std::to_string(this->stagnationLimit) + + " s -- stopping it"); + } else { + this->stoppedForMemory = true; + Map2Check::Log::Warning( + "KLEE halted: the run reached 80% of its memory limit (" + + std::to_string(limitMB) + " MB)"); } - this->stoppedOnStagnation = true; - Map2Check::Log::Warning("KLEE stagnated: no new coverage for " + - std::to_string(this->stagnationLimit) + - " s -- stopping it"); // A KLEE blocked inside a native external call (Juliet's fscanf variants: // __isoc99_fscanf handed a uClibc FILE*) never looks at the interrupt // flag -- nor at its own --max-time -- and used to hold the rest of its // window until timeout's SIGKILL. Not stopped within the grace, it is // killed now and the time goes to the next phase. Nothing is lost: a run - // that stagnated is already counted incomplete. + // that stagnated is already counted incomplete. Writing the tests of the + // live states takes memory too: past 92% it is killed at once. constexpr int kInterruptGraceSeconds = 10; + bool killed = false; for (int tick = 0; tick < 2 * kInterruptGraceSeconds && !done; ++tick) { std::this_thread::sleep_for(std::chrono::milliseconds(500)); - } - if (!done) { - if (klee > 0) { - kill(klee, SIGKILL); - } else if (pid > 0) { - kill(pid, SIGKILL); + if (!done && memoryNow() == Map2Check::MemoryAction::Kill) { + killForMemory(); + killed = true; + break; } + } + if (!done && !killed) { + signalKlee(SIGKILL); Map2Check::Log::Warning( "KLEE did not stop within " + std::to_string(kInterruptGraceSeconds) + @@ -325,7 +400,6 @@ int Caller::runKleeWatched(const std::string &command) { } runner.join(); return result; -#endif } bool Caller::replayKleeVectorsForViolation() { @@ -377,7 +451,8 @@ bool Caller::replayKleeVectorsForViolation() { static_cast(bytes.size())); } std::ostringstream command; - command << "cd '" << replay << "' && timeout -k 1 2 '" << witness + command << nativeMemoryPrefix() << "cd '" << replay + << "' && timeout -k 1 2 '" << witness << "' < input > /dev/null 2>&1"; system(command.str().c_str()); ++replayed; @@ -519,7 +594,8 @@ unsigned Caller::exportFuzzerCorpusAsKtests() { const std::string input = std::filesystem::absolute(queue + "/" + name, error).string(); std::ostringstream command; - command << "cd '" << replay << "' && MAP2CHECK_SEED_REPLAY=1 timeout -k 1 2 '" << witness + command << nativeMemoryPrefix() << "cd '" << replay + << "' && MAP2CHECK_SEED_REPLAY=1 timeout -k 1 2 '" << witness << "' < '" << input << "' > /dev/null 2>&1"; system(command.str().c_str()); @@ -583,7 +659,7 @@ std::vector> Caller::fuzzerCorpusVectors( const std::string input = std::filesystem::absolute(queue + "/" + name, error).string(); std::ostringstream command; - command << "cd '" << replay + command << nativeMemoryPrefix() << "cd '" << replay << "' && MAP2CHECK_SEED_REPLAY=1 timeout -k 1 2 '" << witness << "' < '" << input << "' > /dev/null 2>&1"; system(command.str().c_str()); @@ -1353,13 +1429,23 @@ void Caller::executeAnalysis(std::string solvername) { // KLEE's own default cap is 2,000 MB, well under what a Test-Comp run // gets; past it KLEE kills states and stops forking, and the run can no // longer be TRUE. MAP2CHECK_KLEE_MAX_MEMORY (MB) raises it. + // + // Without the knob the cap follows the run's limit (kleeMaxMemoryMB): + // 1,200 MB of a 3 GB run, KLEE's own 2,000 MB from 5 GB up. KLEE checks + // it only outside seeding; runKleeWatched covers the rest. + bool maxMemorySet = false; if (const char *maxMemory = std::getenv("MAP2CHECK_KLEE_MAX_MEMORY")) { const std::string megabytes(maxMemory); if (!megabytes.empty() && megabytes.find_first_not_of("0123456789") == std::string::npos) { kleeCommand << " --max-memory=" << megabytes; + maxMemorySet = true; } } + if (!maxMemorySet) { + const long long megabytes = Map2Check::kleeMaxMemoryMB(runLimitMB()); + if (megabytes > 0) kleeCommand << " --max-memory=" << megabytes; + } // Halting on the first error is right when there is a property to @@ -1532,6 +1618,8 @@ void Caller::executeAnalysis(std::string solvername) { gotTimeout = true; // Stopped by us for want of progress: states were left, nothing proved. if (this->stoppedOnStagnation) gotTimeout = true; + // Stopped by us for memory: the same, states were left. + if (this->stoppedForMemory) gotTimeout = true; // KLEE exits 0 when its queue empties, like a run that explored every // path -- also after its timer, a concretized input or states it killed // itself. None of those proves anything. Treated as the timeout it is: a @@ -1632,6 +1720,16 @@ void Caller::executeAnalysis(std::string solvername) { command << Map2Check::aflFuzzBinary() << " -i '" << inputDir << "'" << " -o afl-out"; + // afl-fuzz runs its target with no memory limit by default, and one + // execution that allocates gigabytes crosses the run's limit: the + // Test-Comp 2027 pre-run (3 GB) lost 239 runs in the first fuzzer + // phase. With -m such an allocation fails inside the target, as on a + // smaller machine. + { + const long long megabytes = + Map2Check::nativeMemoryLimitMB(runLimitMB()); + if (megabytes > 0) command << " -m " << megabytes; + } if (hasCmplog) command << " -c ./" << programHash << "-cmplog.out"; command << " -- ./" << programHash << "-fuzzed.out" << " > fuzzer.output 2>&1"; diff --git a/modules/frontend/caller.hpp b/modules/frontend/caller.hpp index 49a2530f0..3b2c8e229 100644 --- a/modules/frontend/caller.hpp +++ b/modules/frontend/caller.hpp @@ -203,6 +203,8 @@ class Caller { unsigned stagnationLimit = 0; /** Whether this phase's KLEE was stopped for stagnating: incomplete. */ bool stoppedOnStagnation = false; + /** Whether this phase's KLEE was stopped for the run's memory: incomplete. */ + bool stoppedForMemory = false; /** Where to report how long this phase's engine ran (main sizes the next * alternating phase with it); null: not reported. */ double* engineSeconds = nullptr; diff --git a/modules/frontend/utils/memory_budget.hpp b/modules/frontend/utils/memory_budget.hpp new file mode 100644 index 000000000..5ccee6831 --- /dev/null +++ b/modules/frontend/utils/memory_budget.hpp @@ -0,0 +1,129 @@ +/** + * 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_MEMORY_BUDGET_HPP_ +#define MODULES_FRONTEND_UTILS_MEMORY_BUDGET_HPP_ + +#include +#include +#include +#include + +namespace Map2Check { + +/** The memory a run may use, and how much of it the engines get. + * + * BenchExec enforces its limit on the run's cgroup as a whole: the engines, + * the native replays and the tmpfs that holds every file the tool writes + * ("a RAM disk that is included in the memory limit"). Crossing it ends the + * whole run as OUT OF MEMORY, with no test suite -- even when what crossed it + * was one throwaway process. The Test-Comp 2027 pre-run (3 GB) lost 1,747 + * runs that way. None of the engines knows the limit: KLEE's own cap is a + * fixed 2,000 MB that its seeding loop never checks, and afl-fuzz runs its + * target with no memory limit at all. + * + * Inside BenchExec's container the run's cgroup is the root of the cgroup + * namespace, so /sys/fs/cgroup/memory.max is the limit and memory.current + * what is used, tmpfs included (measured with runexec 3.34). */ + +/** Bytes in `path` (a cgroup v2 memory.max or memory.current), or -1 when it + * is missing, unreadable or "max" (no limit). */ +inline long long readCgroupBytes(const std::string& path) { + std::ifstream file(path); + std::string value; + if (!(file >> value) || value.empty() || + value.find_first_not_of("0123456789") != std::string::npos) { + return -1; + } + return std::stoll(value); +} + +/** The directory of this process's cgroup v2 under `root`, from a + * /proc/self/cgroup listing ("0::/path"); `root` itself when the listing has + * no v2 entry. */ +inline std::string cgroupDirectory(const std::string& root, + const std::string& procCgroup) { + std::ifstream file(procCgroup); + std::string line; + while (std::getline(file, line)) { + if (line.rfind("0::", 0) == 0) { + std::string path = line.substr(3); + if (path == "/") path.clear(); + return root + path; + } + } + return root; +} + +/** Where the run's limit is enforced: the closest cgroup, from this process's + * own up to `root`, whose memory.max holds a number. Empty when none does. */ +inline std::string limitingCgroup( + const std::string& root = "/sys/fs/cgroup", + const std::string& procCgroup = "/proc/self/cgroup") { + std::string dir = cgroupDirectory(root, procCgroup); + while (true) { + if (readCgroupBytes(dir + "/memory.max") > 0) return dir; + if (dir.size() <= root.size()) return ""; + dir = dir.substr(0, dir.rfind('/')); + } +} + +/** The run's memory limit in MB, or 0 when it is unknown. + * MAP2CHECK_MEMORY_LIMIT_MB, when set to a number, wins over the cgroup. */ +inline long long runMemoryLimitMB(const std::string& cgroup) { + if (const char* forced = std::getenv("MAP2CHECK_MEMORY_LIMIT_MB")) { + const std::string value(forced); + if (!value.empty() && + value.find_first_not_of("0123456789") == std::string::npos) { + return std::stoll(value); + } + } + if (cgroup.empty()) return 0; + const long long bytes = readCgroupBytes(cgroup + "/memory.max"); + return bytes > 0 ? bytes >> 20 : 0; +} + +/** KLEE's --max-memory for a run limited to `limitMB`: 40% of it, never above + * KLEE's own default of 2,000 MB -- so a 15 GB run keeps exactly the cap it was + * measured with, and a 3 GB one gets 1,200 MB. 0 means "leave KLEE's + * default". The other 60% is what the tmpfs (seed store, KLEE's output, the + * fuzzer's queue), the frontend and the replays have needed: on the + * Intel-TDX tasks the files alone reached 1 GB. */ +inline long long kleeMaxMemoryMB(long long limitMB) { + if (limitMB <= 0) return 0; + return std::max(256LL, std::min(2000LL, limitMB * 2 / 5)); +} + +/** The address-space limit, in MB, for a program run natively: afl-fuzz's + * target (-m) and the replays of vectors. A third of the run's limit, at + * least 256 MB; 0 when the limit is unknown (no limit, as before). A target + * that allocates past it fails its malloc, as it would on a smaller machine, + * instead of taking the run down with it. */ +inline long long nativeMemoryLimitMB(long long limitMB) { + if (limitMB <= 0) return 0; + return std::max(256LL, limitMB / 3); +} + +/** What the KLEE watchdog does on a reading of the run's memory. */ +enum class MemoryAction { None, Halt, Kill }; + +/** Halt KLEE (SIGINT: it stops and writes its tests) at 80% of the limit; + * kill it at 92%, where writing the tests of the live states could itself + * cross the limit. Both apply to the whole run, because that is what + * BenchExec measures. */ +inline MemoryAction memoryAction(long long usedBytes, long long limitMB) { + if (usedBytes < 0 || limitMB <= 0) return MemoryAction::None; + const long long limit = limitMB << 20; + if (usedBytes >= limit / 100 * 92) return MemoryAction::Kill; + if (usedBytes >= limit / 100 * 80) return MemoryAction::Halt; + return MemoryAction::None; +} + +} // namespace Map2Check + +#endif // MODULES_FRONTEND_UTILS_MEMORY_BUDGET_HPP_ diff --git a/tests/unit/frontend/CMakeLists.txt b/tests/unit/frontend/CMakeLists.txt index 1ff300a70..61eb02bed 100644 --- a/tests/unit/frontend/CMakeLists.txt +++ b/tests/unit/frontend/CMakeLists.txt @@ -31,6 +31,11 @@ add_executable(AlternationTest ) map2check_test(AlternationTest) +add_executable(MemoryBudgetTest + MemoryBudgetTest.cpp +) +map2check_test(MemoryBudgetTest) + add_executable(KleeLogTest KleeLogTest.cpp $ diff --git a/tests/unit/frontend/MemoryBudgetTest.cpp b/tests/unit/frontend/MemoryBudgetTest.cpp new file mode 100644 index 000000000..5ceff32f2 --- /dev/null +++ b/tests/unit/frontend/MemoryBudgetTest.cpp @@ -0,0 +1,115 @@ +/** + * 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 + +#include "../../../modules/frontend/utils/memory_budget.hpp" + +namespace fs = std::filesystem; +using Map2Check::MemoryAction; + +namespace { + +class FakeCgroup : public ::testing::Test { + protected: + void SetUp() override { + root = (fs::temp_directory_path() / + ("m2c-cgroup-" + std::to_string(::getpid()) + "-" + + ::testing::UnitTest::GetInstance()->current_test_info()->name())) + .string(); + fs::remove_all(root); + fs::create_directories(root); + unsetenv("MAP2CHECK_MEMORY_LIMIT_MB"); + } + void TearDown() override { + fs::remove_all(root); + unsetenv("MAP2CHECK_MEMORY_LIMIT_MB"); + } + void write(const std::string& relative, const std::string& content) { + const fs::path path = fs::path(root) / relative; + fs::create_directories(path.parent_path()); + std::ofstream(path) << content; + } + std::string root; +}; + +} // namespace + +// BenchExec's container: the run's cgroup is the namespace root ("0::/"). +TEST_F(FakeCgroup, ReadsTheLimitAtTheNamespaceRoot) { + write("cgroup/memory.max", "2999996416\n"); + write("proc", "0::/\n"); + const std::string dir = + Map2Check::limitingCgroup(root + "/cgroup", root + "/proc"); + EXPECT_EQ(dir, root + "/cgroup"); + EXPECT_EQ(Map2Check::runMemoryLimitMB(dir), 2861); +} + +// A cgroup without a limit of its own ("max") inherits its parent's. +TEST_F(FakeCgroup, WalksUpToTheCgroupThatHasTheLimit) { + write("cgroup/memory.max", "max\n"); + write("cgroup/run/memory.max", "3145728000\n"); + write("cgroup/run/tool/memory.max", "max\n"); + write("proc", "0::/run/tool\n"); + const std::string dir = + Map2Check::limitingCgroup(root + "/cgroup", root + "/proc"); + EXPECT_EQ(dir, root + "/cgroup/run"); + EXPECT_EQ(Map2Check::runMemoryLimitMB(dir), 3000); +} + +TEST_F(FakeCgroup, NoLimitAnywhereIsUnknown) { + write("cgroup/memory.max", "max\n"); + write("proc", "0::/\n"); + const std::string dir = + Map2Check::limitingCgroup(root + "/cgroup", root + "/proc"); + EXPECT_EQ(dir, ""); + EXPECT_EQ(Map2Check::runMemoryLimitMB(dir), 0); +} + +TEST_F(FakeCgroup, NoCgroupFilesystemIsUnknown) { + const std::string dir = + Map2Check::limitingCgroup(root + "/absent", root + "/absent-proc"); + EXPECT_EQ(dir, ""); + EXPECT_EQ(Map2Check::runMemoryLimitMB(dir), 0); +} + +TEST_F(FakeCgroup, TheEnvironmentOverridesTheCgroup) { + write("cgroup/memory.max", "2999996416\n"); + setenv("MAP2CHECK_MEMORY_LIMIT_MB", "15000", 1); + EXPECT_EQ(Map2Check::runMemoryLimitMB(root + "/cgroup"), 15000); + setenv("MAP2CHECK_MEMORY_LIMIT_MB", "lots", 1); + EXPECT_EQ(Map2Check::runMemoryLimitMB(root + "/cgroup"), 2861); +} + +TEST(KleeMaxMemory, FortyPercentOfTheRunNeverAboveKleesDefault) { + EXPECT_EQ(Map2Check::kleeMaxMemoryMB(3000), 1200); + EXPECT_EQ(Map2Check::kleeMaxMemoryMB(15000), 2000); + EXPECT_EQ(Map2Check::kleeMaxMemoryMB(400), 256); + EXPECT_EQ(Map2Check::kleeMaxMemoryMB(0), 0); +} + +TEST(NativeMemoryLimit, AThirdOfTheRun) { + EXPECT_EQ(Map2Check::nativeMemoryLimitMB(3000), 1000); + EXPECT_EQ(Map2Check::nativeMemoryLimitMB(15000), 5000); + EXPECT_EQ(Map2Check::nativeMemoryLimitMB(300), 256); + EXPECT_EQ(Map2Check::nativeMemoryLimitMB(0), 0); +} + +TEST(MemoryAction, HaltsAtEightyAndKillsAtNinetyTwoPercent) { + const long long mb = 1LL << 20; + EXPECT_EQ(Map2Check::memoryAction(2000 * mb, 3000), MemoryAction::None); + EXPECT_EQ(Map2Check::memoryAction(2400 * mb, 3000), MemoryAction::Halt); + EXPECT_EQ(Map2Check::memoryAction(2760 * mb, 3000), MemoryAction::Kill); + EXPECT_EQ(Map2Check::memoryAction(-1, 3000), MemoryAction::None); + EXPECT_EQ(Map2Check::memoryAction(2900 * mb, 0), MemoryAction::None); +} From 82aec4df71ad2466ba9f1d3bf6ccb47d69056ad4 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 7 Nov 2026 03:39:12 -0400 Subject: [PATCH 2/7] docs(changelog): the memory governor and the Cover-Branches disk fix --- CHANGELOG.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 788d9dee6..cf3006f35 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,21 @@ The format loosely follows [Keep a Changelog](https://keepachangelog.com/en/1.0. ## [Unreleased] +### Fixed + +- **The run stays below its memory limit** (Test-Comp 2027 pre-run: 1,747 runs + ended as OUT OF MEMORY at 3 GB). The limit is read from the run's cgroup + (`memory.max`; `MAP2CHECK_MEMORY_LIMIT_MB` overrides it): + - KLEE's `--max-memory` is 40% of the limit, at most KLEE's default + 2,000 MB (a 15 GB run is unchanged); + - a watchdog halts KLEE at 80% of the limit and kills it at 92%, also during + seeding, which KLEE's own cap does not cover; + - the afl-fuzz target (`-m`) and the native replays (`ulimit -v`) get a + third of the limit. +- Cover-Branches: KLEE writes only the tests of paths that covered new code + (`--only-output-states-covering-new`), and the wrapper starts Map2Check with + core dumps off. + ## [9.0.0] - Unreleased A major version: the fuzzing engine changed (LibFuzzer → AFL++ 4.40c), the From dd9f0d8121318f4a3612c85e47843eb5c23068e4 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 7 Nov 2026 04:25:31 -0400 Subject: [PATCH 3/7] fix(afl): no fuzzing target outlives afl-fuzz afl-fuzz starts each forkserver with setsid() (afl-forkserver.c, 4.40c), so its targets sit in sessions of their own, outside the process group `timeout` signals. When `timeout -k` SIGKILLs afl-fuzz, a running target survives and keeps spending the run's CPU time after Map2Check is done: a 900 s BenchExec run ended with 870 s of wall time, 908 s of CPU time and TIMEOUT. A persistent-mode target stopped in raise(SIGSTOP) is also left in an orphaned process group. When afl-fuzz returns, every process whose argv[0] is this program's fuzzing or CmpLog binary (the names carry the program's hash) is killed. test_fuzzer_leftovers.sh: a fake afl-fuzz leaves such a process in a new session and exits. RED: it is still running after map2check; GREEN: gone. --- .github/workflows/ci.yml | 1 + modules/frontend/caller.cpp | 42 +++++++++++++ tests/integration/test_fuzzer_leftovers.sh | 70 ++++++++++++++++++++++ 3 files changed, 113 insertions(+) create mode 100644 tests/integration/test_fuzzer_leftovers.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9d2842740..c5613b70a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -367,6 +367,7 @@ jobs: bash tests/integration/test_target_coverage.sh bash tests/integration/test_ktest_object_names.sh bash tests/integration/test_testcomp_regressions.sh + bash tests/integration/test_fuzzer_leftovers.sh bash tests/integration/test_exit_codes.sh bash tests/integration/test_cwe_mode_mapping.sh ' diff --git a/modules/frontend/caller.cpp b/modules/frontend/caller.cpp index eff9520b8..c755f2eb8 100644 --- a/modules/frontend/caller.cpp +++ b/modules/frontend/caller.cpp @@ -171,6 +171,42 @@ std::string Caller::postOptimizationFlags() { return flags.str(); } +namespace { +/** SIGKILLs every process whose program is one of `names` (argv[0] ending in + * it): what afl-fuzz left of its targets. Returns how many it killed. + * + * afl-fuzz starts each forkserver with setsid() (afl-forkserver.c in 4.40c), + * so the targets live in sessions of their own, outside the process group + * `timeout` signals. When `timeout -k` has to SIGKILL afl-fuzz, a target that + * is running stays alive and keeps burning the run's CPU time after Map2Check + * is done -- measured: 870 s of wall time, 908 s of CPU, TIMEOUT -- and a + * persistent-mode target stopped in raise(SIGSTOP) is left in an orphaned + * process group. The names carry the program's hash, so nothing else + * matches. */ +unsigned killLeftoverTargets(const std::vector &names) { + unsigned killed = 0; + std::error_code error; + for (const auto &entry : + std::filesystem::directory_iterator("/proc", error)) { + const std::string pid = entry.path().filename().string(); + if (pid.empty() || pid.find_first_not_of("0123456789") != std::string::npos) + continue; + std::ifstream cmdline(entry.path() / "cmdline"); + std::string program; + std::getline(cmdline, program, '\0'); + for (const std::string &name : names) { + if (program.size() >= name.size() && + program.compare(program.size() - name.size(), name.size(), name) == + 0) { + if (kill(static_cast(std::stol(pid)), SIGKILL) == 0) ++killed; + break; + } + } + } + return killed; +} +} // namespace + namespace { /** The cgroup whose memory.max limits this run, found once (empty: none). */ const std::string &runCgroup() { @@ -1736,6 +1772,12 @@ void Caller::executeAnalysis(std::string solvername) { const auto engineStarted = std::chrono::steady_clock::now(); int result = system(command.str().c_str()); + // No target outlives its fuzzer (see killLeftoverTargets). + if (const unsigned leftover = killLeftoverTargets( + {programHash + "-fuzzed.out", programHash + "-cmplog.out"})) { + Map2Check::Log::Warning("killed " + std::to_string(leftover) + + " fuzzing target(s) afl-fuzz left behind"); + } if (this->engineSeconds != nullptr) { *this->engineSeconds = std::chrono::duration( std::chrono::steady_clock::now() - diff --git a/tests/integration/test_fuzzer_leftovers.sh b/tests/integration/test_fuzzer_leftovers.sh new file mode 100644 index 000000000..d7b390834 --- /dev/null +++ b/tests/integration/test_fuzzer_leftovers.sh @@ -0,0 +1,70 @@ +#!/bin/bash +# test_fuzzer_leftovers.sh -- no fuzzing target outlives afl-fuzz. +# +# afl-fuzz starts its forkservers with setsid(), so the targets live in +# sessions of their own, outside the process group that `timeout` signals. +# When afl-fuzz is SIGKILLed (timeout -k), a running target survives it and +# keeps consuming the run's CPU time after Map2Check has finished: in a 900 s +# BenchExec run, 870 s of wall time became 908 s of CPU time and a TIMEOUT. +# +# A fake afl-fuzz (MAP2CHECK_AFL_FUZZ) reproduces exactly that: it leaves a +# process named like the target in a new session, then exits. Map2Check must +# kill it when the fuzzer phase ends. + +set -u + +MAP2CHECK_DIR="${MAP2CHECK_PATH:-/workspace/install_e2e}" +WORK=$(mktemp -d) +LEFT="$WORK/leftover.pid" +cleanup() { + [ -s "$LEFT" ] && kill -9 "$(cat "$LEFT")" 2>/dev/null + rm -rf "$WORK" +} +trap cleanup EXIT + +PASSED=0 +FAILED=0 +ok() { echo " PASS $1"; PASSED=$((PASSED+1)); } +fail() { echo " FAIL $1: $2"; FAILED=$((FAILED+1)); } + +echo "=== Fuzzer phase: leftover targets ===" + +cat > "$WORK/afl-fuzz" < "$LEFT"; exec -a "\$0" sleep 300' "\$target" < /dev/null > /dev/null 2>&1 & +for i in \$(seq 1 50); do [ -s "$LEFT" ] && break; sleep 0.1; done +exit 0 +EOF +chmod +x "$WORK/afl-fuzz" + +cat > "$WORK/task.c" <<'EOF' +extern int __VERIFIER_nondet_int(void); +int main(void) { + int x = __VERIFIER_nondet_int(); + if (x > 10) return 1; + return 0; +} +EOF + +(cd "$WORK" && MAP2CHECK_AFL_FUZZ="$WORK/afl-fuzz" \ + "$MAP2CHECK_DIR/map2check" --cover-branches --generate-test-suite \ + --nondet-generator afl --timeout 30 task.c > map2check.out 2>&1) + +if [ ! -s "$LEFT" ]; then + fail "the fake afl-fuzz ran" "no leftover was started (see map2check.out)" + sed -n '1,40p' "$WORK/map2check.out" +else + ok "the fake afl-fuzz left a target behind" + pid=$(cat "$LEFT") + if kill -0 "$pid" 2>/dev/null; then + fail "no target outlives the fuzzer" "pid $pid is still running" + else + ok "no target outlives the fuzzer" + fi +fi + +echo " Results: $PASSED passed, $FAILED failed" +[ "$FAILED" -eq 0 ] From b8a932a326366618a5d0a0ac0f8df71a02f7c42d Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 7 Nov 2026 04:26:59 -0400 Subject: [PATCH 4/7] docs(tacas): log the Test-Comp 2027 pre-run memory round (cgroup governor) --- docs/reports/tacas-experiment-log.md | 66 ++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) diff --git a/docs/reports/tacas-experiment-log.md b/docs/reports/tacas-experiment-log.md index 6f1e0aced..1765b4c0b 100644 --- a/docs/reports/tacas-experiment-log.md +++ b/docs/reports/tacas-experiment-log.md @@ -1377,3 +1377,69 @@ existe, em vez de um `map2check-testcomp.py` à parte. - Ressalvas: uma execução por braço, com a variância do fuzzer; nenhuma sonda local chegou aos 15 GB; não sabemos quais tarefas foram mortas. A seleção da suíte por ordem de chegada e o teto de 50 ficaram na issue #92. + +## Pré-rodada da Test-Comp 2027: memória contra o limite do cgroup (2026-11-07) + +- **Motivo:** os resultados da pré-rodada `map2check.2026-10-29_21-07-49` (BenchExec + 3.35-331, 900 s, **3 GB, 1 núcleo**, VerifierCloud) e os 16 288 logs, todos públicos em + `test-comp.sosy-lab.org/2027/results/results-verified/`: + - 14 507 `ERROR`, 1 747 `OUT OF MEMORY` e 34 `FAILED (KILLED BY SIGNAL 1)`, sem nenhum + `DONE`; + - **os 14 507 `ERROR` terminam com a linha `DONE`.** O módulo tool-info usado era anterior + ao benchexec#1352, mergeado em 02/11. +- **Onde morreram os 1 747 OOM** (última linha e última fase de cada log): + - 1 386 em Cover-Branches e 361 em Cover-Error, espalhados por 22 conjuntos, não só no + TDX (Hardware 671, Combinations 225, Arrays 173, DeviceDrivers 129…); + - **821 no seeding do KLEE.** No KLEE 3.1, o laço de seeding (`Executor::run`) não chama + `checkMemoryUsage()`, então o `--max-memory` não vale ali; + - cerca de 200 com o KLEE no teto de 2 000 MB, o que, somado ao tmpfs, passa de 3 GB; + - **239 na fase 1 do AFL++.** O afl-fuzz roda o alvo sem limite de memória. +- **Os 34 SIGHUP:** todos `*_havoc_memory` do TDX em Cover-Error, em 31 máquinas, com cerca + de 889 s. Os logs param na fase 8 (KLEE), no despejo dos estados após o `HaltTimer`. Sem + medições, o que é compatível com o OOM killer do sistema derrubando o BenchExec (leitura + do Dirk). +- **Sonda de cgroup:** dentro do `runexec` 3.34, `/proc/self/cgroup` mostra `0::/`, e + `/sys/fs/cgroup/memory.max` = 2 999 996 416 (o limite), além de `memory.current`. +- **Correção** (branch `fix/testcomp-memory-governor`, a partir do `develop` `d4f465b47`): + - `utils/memory_budget.hpp` lê o limite do cgroup (`MAP2CHECK_MEMORY_LIMIT_MB` sobrepõe); + - `--max-memory` do KLEE = 40 % do limite, no máximo 2 000 MB (com 3 GB, 1 144 MB; com + 15 GB, igual a antes); + - o vigia do KLEE lê `memory.current` a cada 0,5 s: SIGINT a 80 %, SIGKILL a 92 %. A fase + conta como incompleta; + - o alvo do afl-fuzz (`-m`) e os replays nativos (`ulimit -v`) ficam com um terço do + limite; + - depois de cada fase do AFL++, mata os alvos que sobraram. O afl-fuzz faz `setsid()` no + forkserver (`afl-forkserver.c:1066`), então os alvos ficam fora do grupo do `timeout`. +- **A/B no BenchExec 3.34** (`run.sh generate`, 900 s / 3 GB / 1 núcleo, uma execução por + braço; base = archive do Zenodo 23672409, md5 conferido; correção = `make-archive.sh` do + `install_mg`; pelo CRC, só `map2check` e o wrapper diferem). Cobertura pelo TestCov + (gcc, sem formatação): + +| tarefa | prop. | base | correção (mg) | +|---|---|---|---| +| `data_structures_set_multi_proc_ground-2` | cb | OOM (6 s), suíte inválida | done (328 s), **65,22 %** | +| `btor2c-lazyMod.h_segments` | cb | OOM (79 s), 57,89 % | done (820 s), **84,21 %** | +| `partial_mod_count_limited_1` | cb | OOM (61 s), 85,71 % | TIMEOUT (CPU 909 s, parede 871 s), **92,86 %** | +| `Problem05_label40+token_ring.01.cil-1` | cb | done (612 s), 3,68 % | done (797 s), 3,81 % | +| TDX `tdg_servtd_wr__expected__cover_exit_havoc_object` | ce | OOM (182 s), 0 testes | done (260 s), 0 testes | +| TDX `tdg_mr_report__unconstrained__cover_exit_success_havoc_memory` | ce | done (423 s), 0 testes | done (500 s), 0 testes | + +- **O TIMEOUT:** CPU acima do tempo de parede, com 1 núcleo, indica um processo vivo depois + do wrapper. Numa sonda `runexec` da mesma tarefa, com amostras do `ps` a cada 5 s: + - os forkservers do AFL++ aparecem como líderes de sessão (`Ss`), e os alvos persistentes + ficam parados (`T`); + - nessa execução: `DONE`, 875 s de parede, 558 s de CPU, pico de **2,42 GB**; + - o vigia parou o KLEE nas fases 2, 4 e 6 ("80% of its memory limit"), sempre no seeding. + - Daí o `killLeftoverTargets` e o teste `test_fuzzer_leftovers.sh` (afl-fuzz falso que + deixa um alvo numa sessão nova). RED: o processo sobrevive ao map2check. GREEN: some. +- **Leitura:** + - nas 3 tarefas em que o base dá OOM em Cover-Branches, a correção termina e cobre mais; + - o OOM do TDX havoc_object em Cover-Error desaparece. Nenhum braço acha a violação nessas + duas tarefas, como na rodada de 05/11; + - nada piora. + - Ressalvas: + - uma execução por braço, e a máquina estava em swap ("System has swapped"); + - nesta tarefa, o seeding do KLEE enche a memória em toda fase. O KLEE sobrevive, mas + quase não explora. Um teto no número ou no tamanho das sementes fica como próximo + passo; + - o SIGHUP não foi reproduzido localmente. From 3fec8cefefdf18195517d70c88ee619997f2c3c1 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 7 Nov 2026 05:12:54 -0400 Subject: [PATCH 5/7] fix(wrapper): 30 s between Map2Check's wall-clock budget and the CPU limit Under BenchExec with one core a run's CPU time came out up to 22 s above its wall time (888 s of CPU for 866 s of wall, 900 s / 3 GB). With a 20 s margin the run ended 12 s from a TIMEOUT. --- utils/map2check-wrapper.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/utils/map2check-wrapper.py b/utils/map2check-wrapper.py index 55e8d61c5..0f46b9b56 100755 --- a/utils/map2check-wrapper.py +++ b/utils/map2check-wrapper.py @@ -52,8 +52,13 @@ # 900s is the Test-Comp per-task budget. The tool gets slightly less so that it # is Map2Check that stops and writes its suite, rather than the harness killing # it mid-write and leaving a truncated metadata.xml behind. +# +# The budget is CPU time and Map2Check counts wall time. Under BenchExec with +# one core the run's CPU time came out up to 22 s above its wall time (900 s, +# 3 GB: 888 s of CPU for 866 s of wall), so 20 s of margin left the run 12 s +# from a TIMEOUT. 30 s keeps it clear. DEFAULT_BUDGET = 900 -SHUTDOWN_MARGIN = 20 +SHUTDOWN_MARGIN = 30 def parse_args(argv): From 6cdf263acf3fc2461f554e6b32f222ad424d4862 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 7 Nov 2026 05:17:04 -0400 Subject: [PATCH 6/7] docs(tacas): the mg2 arm, the CPU-over-wall probe and the final package --- docs/reports/tacas-experiment-log.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/docs/reports/tacas-experiment-log.md b/docs/reports/tacas-experiment-log.md index 1765b4c0b..87442f82c 100644 --- a/docs/reports/tacas-experiment-log.md +++ b/docs/reports/tacas-experiment-log.md @@ -1443,3 +1443,25 @@ existe, em vez de um `map2check-testcomp.py` à parte. quase não explora. Um teto no número ou no tamanho das sementes fica como próximo passo; - o SIGHUP não foi reproduzido localmente. +- **Braço mg2** (com `killLeftoverTargets`, mesmas tarefas e limites): as 6 tarefas `done`. + +| tarefa | CPU / parede (s) | cobertura | +|---|---|---| +| `data_structures_set_multi_proc_ground-2` | 465 / 865 | 65,22 % | +| `btor2c-lazyMod.h_segments` | 436 / 839 | 84,21 % | +| `partial_mod_count_limited_1` | 863 / 860 (era TIMEOUT) | 92,86 % | +| `Problem05_label40+token_ring.01.cil-1` | 888 / 866 | 3,90 % | +| TDX havoc_object (ce) | 436 / 833 | 0 testes | +| TDX havoc_memory (ce) | 470 / 886 | 0 testes | + +- **CPU acima da parede:** + - nenhuma das 14 507 execuções oficiais do binário antigo tem isso; + - numa sonda `runexec` do Problem05 sozinho, com amostras do `ps` a cada 1 s: 844,5 s de + CPU para 838,6 s de parede, e só o `map2check` vivo no fim. O excesso grande vinha dos + alvos que sobravam; + - o que resta (até 22 s com a máquina carregada) levou a `SHUTDOWN_MARGIN` do wrapper de + 20 para 30 s: o Map2Check recebe 870 s de parede. +- **Pacote final** (`map2check-mg3.zip`, md5 `c53d5053072baf2461e132ad1a0944ee`): + - em relação ao mg2, pelo CRC, só o wrapper muda; + - smoke test num `ubuntu:24.04` limpo, com `python3` e `gcc-multilib`: passou; + - BenchExec com 120 s: `done`. From 00a3b25999dcb84efa466ddb065911e3300eefd4 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 7 Nov 2026 05:17:22 -0400 Subject: [PATCH 7/7] docs(changelog): leftover fuzzing targets and the wrapper margin --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index cf3006f35..c722917e4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,11 @@ The format loosely follows [Keep a Changelog](https://keepachangelog.com/en/1.0. seeding, which KLEE's own cap does not cover; - the afl-fuzz target (`-m`) and the native replays (`ulimit -v`) get a third of the limit. +- No fuzzing target outlives afl-fuzz: its forkservers run in sessions of their + own (`setsid()`), and a target left running when `timeout -k` killed afl-fuzz + kept spending the run's CPU time after Map2Check finished (a TIMEOUT). +- The wrapper leaves 30 s, not 20, between Map2Check's wall-clock budget and + the CPU limit: under BenchExec the CPU time came out up to 22 s above it. - Cover-Branches: KLEE writes only the tests of paths that covered new code (`--only-output-states-covering-new`), and the wrapper starts Map2Check with core dumps off.