Symbolic bug hunting with KLEE

The program module is textual .ll, which KLEE accepts directly. The compiler lowers it with compile_program_symbolic (crate osprey-codegen), and the CLI prepends target triple = "x86_64-unknown-linux-gnu" and its data layout on every host — KLEE's varargs lowering is x86-64 only, and an arm64 triple gives false ptr.err reports — then appends @osp_hunt_input_bytes = global i64 <N> so the --input-bytes cap reaches the mock's streams.

• --libc=klee links KLEE's own small libc (strlen, strcmp, strncmp, strchr, strrchr, strcpy, strncpy, strcat, strtol, strtoul, atoi, calloc, abort, atexit, errno, tolower, toupper, memchr, mempcpy) and its freestanding memcpy, memmove, memset, memcmp. The mock library defines only what those two lack (SYMEX-MOCK-STATELESS). --libc=uclibc and --posix-runtime are never used; the macOS package does not build them.
• --external-calls=none makes any call that reaches outside the module an error instead of a native call: KLEE reports it as a user.err whose message begins external calls disallowed, which the tool classifies as unmodelled. KLEE still lets printf and puts with concrete arguments through under this policy, so the mock defines both.
• --ubsan-runtime pairs with the runtime bitcode's -fsanitize=undefined (SYMEX-RUNTIME-BITCODE).
• --kdalloc is KLEE's deterministic allocator with a quarantine that keeps freed addresses out of reuse, which is what makes use-after-free visible and findings identical between runs. The fixed --rng-initial-seed is KLEE's default, stated so the determinism claim in SYMEX-HOSTS has a named source.
• --search=dfs finishes one symbolic path before selecting another instead of leaving a large interleaved working set unfinished when a finite exploration approaches its budget.
• --solver-backend=z3 answers the bit-vector queries the runtime's integer formatting and bounded decimal fold generate several times faster than the default STP backend, which is the difference between finishing a finite exploration inside the budget and stranding its last paths.
• --solver-optimize-divides rewrites constant divisions before the solver sees them; the decimal emitters divide by concrete powers, and the rewritten forms solve faster.
• --emit-all-errors writes a test for every error, not one per (error, instruction) pair, so deduplication is the tool's (SYMEX-FINDINGS) and not KLEE's.
• --optimize runs KLEE's own passes over the unoptimised module, as its documentation recommends for non-trivial programs.
• --max-solver-time=30s bounds one solver query. --max-time is checked between instructions, so without it a single hard query could outlive the budget; a query that hits the bound ends its path as "incomplete", not as a finding.
• The tool kills the engine itself if it has not exited within the budget plus 120 seconds of grace for loading, linking and optimising a large module, and reports that as a toolchain error. KLEE's stderr is captured to a file, never a pipe, so a chatty run cannot stall on a full pipe.

Mock C library

It lives in compiler/runtime/klee/: hunt_stream.c (the one stateful model), hunt_libc.c (stateless doubles), hunt_math.c (libm), hunt_format.c + hunt_decimal.c (the printf family and its exact decimal expansion), hunt_unsupported.c (the stubs), with headers under include/. It includes only headers it defines itself, plus its own klee/klee.h stand-in, so the library builds without KLEE installed. Every exported function is one of the models below or an unsupported stub, and the [SYMEX-MOCK-CLOSED] check — llvm-nm --undefined-only over the linked runtime bitcode, accepting only what KLEE itself provides (its intrinsics, UBSan handlers, allocator and --libc=klee) — runs inside _runtime_klee and fails the build on any symbol the mock forgot.

hunt_mock_tests.c holds the native unit tests and the shared harness (hunt_mock_tests.h), run on the host by make _test_hunt_mock (part of make test), with a shim standing in for KLEE so symbolic bytes come from a queue the test fills and every klee_range name is recorded. Each check asserts the call reaches the mock's double. hunt_mock_format_tests.c drives the printf engine through hand-written integer, string, * and non-finite rows and a 1,296-row float matrix (hunt_format_cases.inc, written by scripts/oracles/hunt_format.py from CPython's correctly rounded formatting), plus every truncation cap. hunt_mock_stream_tests.c drives every stream cap against every symbolic length, every read shape, seeks from every origin, fresh streams per open, open failure, the slot limit, modes, the standard descriptors, and the entropy, clock and object names. The float formatter was differential-fuzzed against the host libc with 200,000 random doubles across 18 formats, with zero mismatches.

Headers — [SYMEX-MOCK-HEADERS]

include/ provides the 19 system headers the portable runtime includes (assert.h, ctype.h, errno.h, fcntl.h, inttypes.h, math.h, pthread.h, signal.h, stdio.h, stdlib.h, string.h, time.h, unistd.h, sys/random.h, sys/select.h, sys/stat.h, sys/time.h, sys/types.h, sys/wait.h), declaring only what the runtime uses. Freestanding headers that clang supplies (stdint.h, stddef.h, stdarg.h, stdbool.h, float.h, limits.h, stdatomic.h) come from clang's resource directory rather than being rewritten.

Byte streams: the one stateful model — [SYMEX-MOCK-STREAM]

A stream is a malloced buffer of the cap's bytes made symbolic with klee_make_symbolic, a length from klee_range(0, cap + 1, name), and a cursor. Reads copy from the cursor and return the short count or 0 once the cursor reaches the length. The cap is --input-bytes, which the CLI writes into the program module as @osp_hunt_input_bytes, overriding the mock's weak default.

These are the only stateful mocks. Read-until-EOF loops (osp_input, readFile's short-read loop in file_runtime.c) never terminate if reads don't track a cursor, so stateless reads would turn every input loop into path explosion. Files keep no state between opens: a file written and then reopened reads back as fresh symbolic content. That over-approximates, and replay filters out any false positive it causes.

File witnesses carry the fixed integer marker osprey.hunt.files.v2 = 2. The decoder uses this marker to select the namespaced format; a filename prefix alone does not select it. A legacy file with that marker-like name still has its own .len metadata and remains a file.

Symbolic read buffers — [SYMEX-MOCK-READ-BUFFER]

readFile uses the configured, clamped stream cap plus two bytes for its initial buffer in a symbolic build: one byte beyond the maximum possible read forces a short read, and one holds the terminator. Allocating the native 64 KiB buffer instead caused a symbolic terminator write to send a 64 KiB array to the solver even for a one-byte input. The cap does not reduce the modeled input beyond --input-bytes. Ordinary native builds retain their 64 KiB initial chunk and growth behavior. Mock tests cover negative, zero, small, maximum and oversized caps; the real file-input crash case must finish and reproduce within ten seconds.

Stateless models — [SYMEX-MOCK-STATELESS]

Unsupported stubs — [SYMEX-MOCK-UNSUPPORTED]

fork, execl, execvp, popen, pclose, pipe, dup2, waitpid, kill, select, pthread_create, pthread_join, pthread_detach, stat and mkdir — processes, threads, descriptor plumbing and the filesystem metadata API — each end their path with klee_report_error(__FILE__, __LINE__, "unmodelled: <name>", "unmodelled.err"). KLEE writes those as test<N>.unmodelled.err, kept apart from real bugs, so you can see where the mock stops being accurate. The native coroutine runtime behind dynamic control handlers (effects_coro.c, one pthread per resumable region) is outside the module for the same reason, so a program that installs such a handler stops at the region's entry with external call outside the module: __osprey_coro_new; static handlers are unaffected. Exploring resumable regions needs a single-stack lowering of them for the symbolic build, which is not built (plan 0034).

Findings and replay

Classes — [SYMEX-FINDINGS]

Each finding is one test<N>.<suffix>.err file in KLEE's output directory, paired with the concrete bytes of every symbolic object from its test<N>.ktest, which the tool parses itself. The suffixes are KLEE's own (TerminationTypes.h, klee_div_zero_check.c, klee_overshift_check.c):

The .early files (interrupted, max depth, out of memory) and unknown suffixes such as model.err and solver.err are not findings; the report counts them under "incomplete", grouped by reason, and --json carries them so a corpus run can tell "clean" from "ran out of time".

Findings are deduplicated by class and the top Osprey frame (or the top C frame, or the message when there is neither). The report lists the class, the Osprey file:line from the top Osprey frame in KLEE's stack, the top C runtime frame, the concrete stdin and file bytes, and the replay verdict. A project's modules share one flattened line numbering in the compiled module, so for a project the tool maps that line back to the module file it was written in and reports that file's own path and line, the same mapping the checker's diagnostics use; a single-file program keeps the name its debug metadata carries. --json writes the same data for CI and the editor: program, engine ("KLEE"), memory ("gc" or "arc"), budgetSeconds, inputBytes, explored{paths,completed,instructions,elapsed}, findings[{test,class,suffix,message,file,line,runtimeFrame,stdin,files[{path,bytes}],replay,replayDetail}], incomplete[{test,reason}], and context as described in [SYMEX-REPORT-HTML].

Managed Osprey operations do not expose unchecked indexing or null dereferences. A memory failure on those paths points to the compiler, runtime or symbolic model. Explicit C calls can introduce failures outside that boundary: tests/hunt/crash.osp intentionally aborts on "9". An abort finding alone therefore does not establish a compiler defect. unmodelled findings identify operations the model cannot execute.

Native replay — [SYMEX-REPLAY]

Each finding is run again on the normal native build — a release build of the program, made once per hunt — on the host running the command:

• the recorded stdin bytes are piped to the process's stdin;
• each recorded file is written at its relative path inside a scratch working directory; a path outside that directory is refused and the finding is skipped with the reason;
• unmodelled findings are skipped: they only exist under KLEE.

Keep every recorded witness until replay. For each class and source location, try later inputs when an earlier input does not reproduce; stop redundant replay once a witness reproduces. Deduplicate the final report after replay, retaining a reproduced witness and its exact stdin and file bytes in preference to a KLEE-only or skipped witness. With --no-replay, retain the first witness per class and location.

A signal death is reproduced; a clean exit — including a non-zero main the program chose itself, even one at or above 128 — is klee-only. The verdict reads the process's signal status, not a folded exit byte, so exit(139) is the program's choice and SIGSEGV is a reproduction. unmodelled findings are marked skipped whether or not any other finding was run. A native run that has not exited after 30 seconds (a server, a prompt loop) is killed and the finding is skipped with that reason. klee-only findings are reported but don't fail the command; they are usually mock over-approximation. Replay through KLEE's libkleeRuntest — harness arguments rebuilt by the entry point, entropy and clock served from a provider over the same recorded objects — is not implemented.

Regression tests — [SYMEX-REGRESSION]

Not built. Every reproduced finding will be written to tests/regressions/klee/<file>_<fn-or-main>_<class>.osp, with the concrete input as literals and an .expectedoutput holding the correct output. The tool can't know what the correct output is, so it will write a placeholder that fails until a human fills it in, and the test stays red until the bug is fixed (the test-first rule in AGENTS.md). Running the tool again never overwrites an existing test. The .ktest will be kept beside the test so --seed-file can start a later run from it.

Human and AI reports — [SYMEX-REPORT-HTML]

Every completed analysis saves report.html and report.json by default, including analyses with findings or unfinished paths. Text mode prints their absolute paths. Open the HTML file directly in a browser; it embeds the Osprey design tokens and needs no network connection or JavaScript. Report write failures are explicit tool errors (exit 2). Compilation and engine failures before analysis completes retain their existing diagnostics and do not produce a findings report.

The HTML explains each finding in plain English, identifies the source line, shows the relevant input and gives a next step. It distinguishes a reproduced native crash, an unconfirmed engine finding, an unsupported operation and unfinished exploration. An unsupported pipe operation means Hunt cannot simulate process spawning; increasing the time budget cannot add that support. No findings is not proof of correctness.

The expandable For AI section embeds the complete JSON, including every finding, replay verdict and detail, input, incomplete path, exploration count and budget. The additional context object records compiler version, engine executable and arguments, runtime bitcode, memory cap, replay setting, working directory, engine stderr, raw error and early-stop reports, engine info/messages/warnings, available source text, and every named symbolic object and its exact bytes for each finding (including entropy and clock inputs). Missing source text is recorded explicitly. Source text and diagnostic strings are HTML-escaped. These local artifacts contain source contents and paths; review them before sharing. The report links to this reference and the KLEE documentation for deeper explanation.

Path accounting — [SYMEX-REPORT-PATHS]

explored.paths counts different executions reached by the engine, not repeated attempts. explored.completed counts normal exits and excludes paths ending in a finding or interruption. Four explored paths, three normal exits, one detected/reproduced crash and zero unfinished paths is successful detection. The HTML shows separate Paths explored and Normal exits metrics, without suggesting a test pass ratio. Findings are deduplicated, so their number need not equal the number of failing paths. Native reproductions, unsupported operations and incomplete paths remain separate outcomes. An exit status of zero alone does not prove completion.

Planted crash gate — [SYMEX-CRASH-GATE]

tests/hunt/crash-cases.json pins fifteen input cases across Default, ML and Python flavor: stdin, parsing, checked arithmetic, lists, maps, closures, recursion, unions, record invariants, JSON, file input, invalid C free and C double free. scripts/hunt_crashes.py runs each program independently and asserts its exact expected finding set, source locations, concrete inputs and native signals. Every finding must reproduce, each case must include a normal symbolic path, and benign stdin Z must exit normally with exact expected output. Missing or corrupt KTEST inputs are reported as skipped and are never replaced with invented empty input. Incomplete exploration, tool errors, missing findings, wrong inputs, KLEE-only results and skipped replay fail. Deliberate C-boundary misuse is labeled as planted, not mistaken for an unexpected compiler defect.

make hunt-crashes builds prerequisites and calls the strict _test_hunt_crashes target. CI installs KLEE and builds its runtime before this target in the existing required macOS coverage job. The required C-runtime job runs the mock and corpus tooling assertions through _test_hunt_mock. Missing KLEE fails the planted-crash gate; it has no skip path. Reports are uploaded as hunt-crash-reports.

Corpus — [SYMEX-CORPUS]

scripts/hunt_corpus.sh runs osprey hunt over every .osp/.ospml under tests/ and examples/ (skipping tests/hunt/ and failscompilation), in parallel, writing one JSON report per program; scripts/hunt_summary.py renders the table. Programs listed in tests/HUNT_UNPORTABLE.txt — one program and reason per line, the same format as tests/WASM_UNPORTABLE.txt — are skipped unless --all is given. make hunt FILE=<path> wraps one run, and make hunt-corpus sweeps the corpus. The corpus runs main mode only. A finding in the corpus is a defect; an "incomplete" result is not. A historical 2026-10-24 sweep covered 224 programs with no findings and 20 cut at the 20-second budget. Those unfinished runs were not proven clean. This sweep is not a required CI check.

Quick corpus qualification — [SYMEX-CORPUS-QUICK]

scripts/hunt_sample.py inventories runnable programs under tests, examples, Book/examples, packages, registry and benchmarks, using the shared hunt_programs.py inventory. Each manifest app is one program; its individual modules, libraries without an entry point and deliberate compilation-rejection examples are excluded. Standalone Default/ML files, Python files carrying the Osprey flavor header, and Python-entry projects are included. Known unportable programs are attempted and reported, rather than silently dropped.

The whole CLI invocation, including compilation, engine execution and native replay, has a ten-second wall-clock deadline. The runner starts a separate process session and kills its process group on timeout. Default engine budget: eight seconds; symbolic input cap: two bytes per stream; concurrency: four. These are explicit sampling bounds, not an exhaustive check of arbitrary input sizes. The compiler and runtime are snapshotted and fingerprinted so concurrent rebuilds do not change a sweep's executable midway through.

A candidate must exit zero within ten seconds, explore at least one path, complete every explored path normally and have no findings or unfinished paths. Timeout, compile/tool error, malformed/missing report, unsupported operation, any finding or incomplete exploration excludes it. index.html, results.json, excluded.json, exact per-program commands/logs and quick-corpus.txt make the result reviewable. The candidate list is a proposed CI corpus; timing on one host is not a guarantee on another. Generated reports stay local.

Editor

The VSCode extension's Osprey: Hunt for Bugs command (osprey.hunt, on the editor context menu and command palette for .osp and .ospml files) saves the active file, runs osprey hunt <file> --json --quiet --max-time <osprey.hunt.maxTime> with the same compiler the language server resolved, prints the report in the "Osprey Hunt" output channel, and publishes every finding as a diagnostic at its Osprey line with source "Osprey Hunt (KLEE)": a reproduced finding is an error, a klee-only or unreplayed one a warning, an unmodelled one information. A missing engine is reported with the brew install klee hint.

Hosts — [SYMEX-HOSTS]

The bitcode is the same on every host (SYMEX-RUNTIME-BITCODE), KLEE's allocator and searcher seed are fixed (SYMEX-KLEE-INVOCATION), so the same program and budget produce the same findings everywhere, up to the time limit.

Delivery checklist

Tests are written first at each step. The compiler items are specified in KLEE code generation.

• [x] Mock library: headers, the stream model, stateless models and unsupported stubs, with native unit tests (make _test_hunt_mock, part of make test) and the [SYMEX-MOCK-CLOSED] undefined-symbol check inside _runtime_klee (part of make build).
• [x] _runtime_klee builds the runtime bitcode from the shared WASM_RT_SRC list (minus web_runtime and wasm_builtins_runtime) plus the mock, with KLEE's clang.
• [x] Symbolic codegen (compile_program_symbolic; there is no --klee CLI flag): abort() on fatal paths, debug metadata on, no optnone. The planned llvm-as parse check over the corpus is not built; KLEE itself parses the module on every hunt.
• [ ] osprey hunt main mode completion proof: the command is implemented, but the unchanged deterministic and default-budget gates must complete every path before this item closes. Deterministic programs under tests/hunt/, each with an .expected file, run by make _test_hunt (part of make test when KLEE is installed) — crash.osp finds input "9" and reproduces its planted C abort at line 4; clean.osp expects no findings; process.osp expects one unsupported-operation finding. Fixed compiler/runtime regressions remain separate controls. The harness rejects incomplete exploration rather than treating it as a passing control.
• [ ] libkleeRuntest replay, including the entropy/clock provider, on top of the native stdin/file replay that ships today; tested by a planted bug that only fires on one symbolic random byte.
• [ ] [SYMEX-HARNESS-TYPED]: a planted bug in a function taking List<int> and a union must be found with --fn; --all-fns lists skips with reasons. Not built.
• [ ] [SYMEX-REGRESSION] test generation. Not built.
• [ ] make hunt-corpus with tests/HUNT_UNPORTABLE.txt: the script and skip list exist. The recorded 224-program run found no findings, but only 204 programs completed and 20 hit the budget. A fully completed run and a required check remain open.
• [ ] Windows: WSL2 run plus --replay-host=windows. Not yet implemented.
• [ ] [SYMEX-PROOF]: the eight cases in four languages, run.sh, report.py with a unit test, and a checked-in results/results.json that meets all four superiority conditions. make ci re-renders the README from the JSON and fails on drift. This item closes last and gates the claim in the comparison table.