fix(testcomp): the archive's AFL++ phase needs gcc-multilib on the host

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.

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

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) {

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):

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() { # <program> <property> <budget>
   echo "$work"
 }
 
+fail() { # <work> <message>
+  echo "FAIL $2" >&2
+  cat "$1/run.log" >&2
+  rm -rf "$1"
+  exit 1
+}
+
+# The run log must show that <engine> ran: map2check prints this line only
+# after the engine's binary (AFL++) or bitcode (KLEE) was built.
+ran() { # <work> <program> <engine>
+  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 "<input>42</input>" "$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 "<input>42</input>" "$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"