From 7609c3bf28faf97fb93c6d9957c7b813ad832948 Mon Sep 17 00:00:00 2001 From: Guilherme Bernardo Date: Sat, 24 Oct 2026 15:54:51 -0400 Subject: [PATCH] fix(testcomp): the archive's AFL++ phase needs gcc-multilib on the host On a clean Ubuntu 24.04 with only python3, the AFL++ binary of the program failed to link: the bundled clang finds no ld, crt1.o, libc or libgcc. The tool does not stop on it -- it skips the fuzzer, gives the whole budget to KLEE and still writes a suite -- so the smoke test passed and every run in the competition would have been KLEE-only. - README: the host needs python3 and gcc-multilib (linker, C runtime and libgcc for 64 and 32 bits); how the engines alternate and what each property's suite holds. - smoketest.sh: fails unless the log shows AFL++ ran (both examples) and KLEE ran (Cover-Branches); the Cover-Branches budget goes from 30 to 60 s, since 30 left KLEE no window. - examples/cover_error.c: defines reach_error, as sv-benchmarks does; an extern-only declaration does not link natively for AFL++. - the wrapper's docstring named the 8.x suite sources. Checked on the rebuilt archive: the smoke test fails on ubuntu:24.04 with only python3, passes with python3 and gcc-multilib on ubuntu:24.04 and 26.04; TestCov 3.11 (the Test-Comp archive) scores the examples' suites TRUE and 100% branch coverage in LP64 and ILP32. Co-Authored-By: Claude Opus 5.5 (1M context) --- utils/map2check-testcomp-wrapper.py | 12 +++-- utils/testcomp-archive/README.txt | 25 +++++++-- utils/testcomp-archive/examples/cover_error.c | 6 ++- utils/testcomp-archive/make-archive.sh | 2 + utils/testcomp-archive/smoketest.sh | 54 +++++++++++++------ 5 files changed, 73 insertions(+), 26 deletions(-) diff --git a/utils/map2check-testcomp-wrapper.py b/utils/map2check-testcomp-wrapper.py index eeb4913d5..006f9ef53 100755 --- a/utils/map2check-testcomp-wrapper.py +++ b/utils/map2check-testcomp-wrapper.py @@ -15,10 +15,12 @@ directory reads as a crashed tool, an empty suite as an honest zero * exit 0 means "I ran"; it does not claim the suite covers anything -Both Test-Comp goals are supported, from two different sources: +Both Test-Comp goals are supported, with AFL++ and KLEE taking turns: - cover-error klee_log.csv, the violating input vector - cover-branches klee-last/*.ktest, one input vector per path KLEE explored + cover-error one test case, the violating input vector of whichever + engine reached reach_error first + cover-branches up to 50 test cases: the fuzzer's corpus (at most half) and + one input vector per path KLEE explored """ import argparse @@ -105,10 +107,10 @@ def main(argv): prop = read_property(args.propertyfile) if COVER_ERROR in prop: - # One test case: the violating vector, from klee_log.csv. + # One test case: the violating vector. goal_flags = ["--target-function", "--target-function-name", "reach_error"] elif COVER_BRANCHES in prop: - # One test case per path KLEE explored, from its own .ktest output. + # The fuzzer's corpus and one test case per path KLEE explored. # No target function: the goal is to cover branches, and asking the # tool to hunt for reach_error would make it stop at the first error # instead of exploring. diff --git a/utils/testcomp-archive/README.txt b/utils/testcomp-archive/README.txt index fbf77f6a7..a6099f321 100644 --- a/utils/testcomp-archive/README.txt +++ b/utils/testcomp-archive/README.txt @@ -21,11 +21,30 @@ it so that the suite is complete. ./map2check-testcomp-wrapper.py --version prints the version ./smoketest.sh runs the two examples in examples/ -The archive is self-contained for x86_64 Ubuntu 24.04: it carries LLVM 16 -(clang, opt, llvm-link), KLEE 3.1 with klee-uclibc, AFL++ 4.40c and every -shared library they need except glibc; it needs python3 on the host. +The archive runs on x86_64 Ubuntu 24.04: it carries LLVM 16 (clang, opt, +llvm-link), KLEE 3.1 with klee-uclibc, AFL++ 4.40c and every shared library +they need except glibc. The host needs two packages: + + apt-get install python3 gcc-multilib + +python3 runs the wrapper. gcc-multilib brings the linker, the C runtime and +libgcc, for both 64 and 32 bits (ILP32 tasks): the bundled clang links the +AFL++ binary of the program with them. Without them the tool still runs and +writes a suite, but skips the fuzzer and leaves the whole budget to KLEE +(the log says "the AFL++ binary failed to build"); ./smoketest.sh fails. The tool can be run from any directory. +How it runs +----------- +Map2Check alternates the two engines in windows until the budget ends, each +seeding the other: AFL++ fuzzes a natively compiled, instrumented binary of +the program, and KLEE explores its bitcode symbolically, starting from the +fuzzer's inputs. Cover-Error stops at the first input that reaches +reach_error, replays it and writes it as the only test case. Cover-Branches +runs until the budget ends or KLEE has explored every path, and writes at most +50 test cases: up to half from the fuzzer's corpus (the inputs that found new +edges), the rest one per path KLEE explored. + Bundled components ------------------ Map2Check GPL-2.0 LICENSE diff --git a/utils/testcomp-archive/examples/cover_error.c b/utils/testcomp-archive/examples/cover_error.c index 9e159c195..89b569388 100644 --- a/utils/testcomp-archive/examples/cover_error.c +++ b/utils/testcomp-archive/examples/cover_error.c @@ -1,4 +1,8 @@ -extern void reach_error(void); +extern void __assert_fail(const char *, const char *, unsigned int, + const char *) __attribute__((__noreturn__)); +/* As in sv-benchmarks: reach_error is defined, so that the program links + natively for the AFL++ phase, and not only as bitcode for KLEE. */ +void reach_error(void) { __assert_fail("0", "cover_error.c", 5, "reach_error"); } extern int __VERIFIER_nondet_int(void); int main(void) { diff --git a/utils/testcomp-archive/make-archive.sh b/utils/testcomp-archive/make-archive.sh index 386f8642c..21a137d3f 100755 --- a/utils/testcomp-archive/make-archive.sh +++ b/utils/testcomp-archive/make-archive.sh @@ -2,6 +2,8 @@ # Builds the Test-Comp tool archive: a self-contained Map2Check directory that # runs on the competition machines (Ubuntu 24.04, clang 18, no LLVM 16, no KLEE, # no AFL++), zipped as the competition expects (one top-level directory). +# The host provides only python3 and gcc-multilib, the linker and C runtime +# that AFL++'s native build needs (required_ubuntu_packages in FM-Tools). # # Run inside the development image, where the install and its dependencies # live (Dockerfile.dev, or map2check-dev:aflpp): diff --git a/utils/testcomp-archive/smoketest.sh b/utils/testcomp-archive/smoketest.sh index 9576fc126..6db3e0170 100755 --- a/utils/testcomp-archive/smoketest.sh +++ b/utils/testcomp-archive/smoketest.sh @@ -1,8 +1,13 @@ #!/bin/sh # Smoke test of the Test-Comp archive (required by the FM-Tools CI): runs # Map2Check on the two examples in examples/, one per Test-Comp property, and -# checks that each run writes a test suite in the exchange format. Exits 0 -# only if both do. +# checks that each run writes a test suite in the exchange format and that the +# engines ran: AFL++ in both, KLEE in Cover-Branches. Exits 0 only if all do. +# +# The engine checks matter because a missing host package does not stop the +# tool: without a native linker and C runtime (gcc-multilib) the AFL++ binary +# fails to build, Map2Check gives the whole budget to KLEE, and a suite is +# still written. set -eu HERE=$(cd "$(dirname "$0")" && pwd) @@ -32,26 +37,41 @@ run() { # echo "$work" } +fail() { # + echo "FAIL $2" >&2 + cat "$1/run.log" >&2 + rm -rf "$1" + exit 1 +} + +# The run log must show that ran: map2check prints this line only +# after the engine's binary (AFL++) or bitcode (KLEE) was built. +ran() { # + case "$3" in + AFL++) line="Executing AFL++ with map2check" ;; + KLEE) line="Executing Klee with map2check" ;; + esac + grep -q "$line" "$1/run.log" || fail "$1" "$2: $3 did not run" +} + # Cover-Error: the suite must hold a test case with the input that reaches -# reach_error (x == 42). +# reach_error (x == 42). AFL++ finds it in its first window, so KLEE is not +# required here. work=$(run cover_error.c coverage-error-call.prp 60) -if ! grep -q "42" "$work"/test-suite/testcase-*.xml 2>/dev/null; then - echo "FAIL cover_error.c: no test case with the input 42" >&2 - cat "$work/run.log" >&2 - rm -rf "$work" - exit 1 -fi +ran "$work" cover_error.c AFL++ +grep -q "42" "$work"/test-suite/testcase-*.xml 2>/dev/null || + fail "$work" "cover_error.c: no test case with the input 42" echo "ok cover_error.c" rm -rf "$work" -# Cover-Branches: the suite must hold at least one test case. -work=$(run cover_branches.c coverage-branches.prp 30) -if ! ls "$work"/test-suite/testcase-*.xml > /dev/null 2>&1; then - echo "FAIL cover_branches.c: no test case" >&2 - cat "$work/run.log" >&2 - rm -rf "$work" - exit 1 -fi +# Cover-Branches: both engines take a turn, and the suite must hold at least +# one test case. A smaller budget leaves no window for KLEE after AFL++'s; +# the run still ends in seconds, once KLEE has explored the four paths. +work=$(run cover_branches.c coverage-branches.prp 60) +ran "$work" cover_branches.c AFL++ +ran "$work" cover_branches.c KLEE +ls "$work"/test-suite/testcase-*.xml > /dev/null 2>&1 || + fail "$work" "cover_branches.c: no test case" echo "ok cover_branches.c" rm -rf "$work"