Repository navigation
Replace the C runtime with map2check-library (Rust) - #76
Merged
Merged
Conversation
… --timeout in the corpus runner
…ests RuntimeABI.hpp/.cpp is the single place that names the runtime functions the passes emit: every RuntimeHook maps to a core symbol of map2check-library and its exact LLVM type, as given by docs/cutover/abi-mapping.tsv and map2check.h. Hooks whose core is '-' (the _uint binops, check_deref, overflowError) are not in the table. tests/unit/pass checks the table against a vendored copy of the mapping (RuntimeABI.*) and, per hook, the IR each pass emits (PassIR.*). The PassIR tests of the passes are red until each pass is migrated. kProgramUnwindFlags names the -fexceptions flag of D1 condition 11.
TrackBasicBlockPass calls the core map2check_save_basic_block_log(line, function) through RuntimeHook::TrackBB instead of the C runtime's map2check_track_bb; the argument order is unchanged and the returned bbtrack_log_t* is ignored. The plugin could not be loaded by opt: it referenced SourceCodeHelper::getLine without linking tools.cpp, and its default constructor (the one the plugin registration uses) leaves the source helper null, which the empty-line walk dereferenced. Link tools.cpp and log.cpp into the plugin and treat every line as non-empty when there is no source helper.
AssertPass calls the core map2check_is_valid_assert(line, function, expression) through RuntimeHook::Assert instead of the C runtime's map2check_assert(cond, line, function): the condition moves from first to last. __assert_fail still passes its line and function with a constant-false condition. A __VERIFIER_assert declared with a non-i32 integer parameter passes "condition != 0" widened to i32.
TargetPass calls the core map2check_reach_target(function, scope, line) through RuntimeHook::TargetReached instead of the C runtime's map2check_target_function; the argument order is unchanged. The core records TARGET-REACHED and returns instead of aborting.
LoopPredAssumePass calls the core __VERIFIER_assume(i32) through RuntimeHook::Assume instead of the C runtime's map2check_assume_loop(i1): the negated loop predicate is zero-extended from i1 to i32.
…kLibrary Map2CheckLibrary calls the core map2check_set_mode(<mode>) and then map2check_init() at the entry, and map2check_success() before returns, exit and abort, through RuntimeHook::SetMode/Init/Success. init no longer takes the dead isSvComp argument of the C runtime. The mode comes from the new -m2c-analysis-mode option (none, memtrack, memcleanup, overflow, assert, target; AnalysisMode values 0-5, default none). The frontend passes it for every run: cover-branches is none and reachability is target. The C runtime got the mode from the AnalysisMode*.bc it linked; the Rust runtime is one library for every mode. LibraryFunctions.hpp, whose only remaining user was this pass, is gone with the C names it declared.
…tions map2check-library rejects a fuzzer input whose __VERIFIER_assume fails by unwinding through the program's frames (D1 condition 11). Without -fexceptions clang marks every C function nounwind, and unwinding through a nounwind function is undefined in LLVM IR; the attributes travel in the bitcode, so the flag belongs on the -emit-llvm step. Every place where the program's C becomes bitcode now passes Map2Check::kProgramUnwindFlags: the -compiled.bc compile, the weak target stub linked after slicing, the wasm entry wrapper and both WasmLifter clang runs. No step adds -fno-unwind-tables or -fno-asynchronous-unwind-tables. The Clam route (--add-invariants) compiles through clam.py and is not changed.
runtimeAnalysisMode moves from a Caller static to an inline function in caller.hpp, next to the new kDefaultMode (MEMTRACK, the mode of a run without a mode flag, now used by map2check.cpp). AnalysisModeTest checks that every frontend mode maps to its number (MEMTRACK 1, MEMCLEANUP 2, OVERFLOW 3, ASSERT 4, REACHABILITY 5, COVER_BRANCHES 0, default 1), and PassIR/FrontendMode feeds each value through opt and checks the constant map2check_set_mode receives.
clam.py compiles the C itself and cannot forward clang flags, so with --add-invariants (ENABLE_CLAM=ON, reachable by AFL++) the program bitcode was nounwind, against D1 condition 11. compileWithClam now compiles the preprocessed C with the flags clam.py would use (-disable-O0-optnone, -fdeclspec, -fno-discard-value-names, -m64, -g, its include dir) plus kProgramUnwindFlags, and hands clam.py the bitcode, for which it skips its own clang step. On a loop program the same 8 verifier.assume calls are injected, and main is no longer nounwind.
…OverflowPass
OverflowPass now declares map2check_binop_{add,sub,mul,div,rem}_signed
through RuntimeABI and calls them with the core order (a, b, bits, line,
fn): operands sign-extended to i64, the operation's own width, no scope.
The _uint variants (C no-ops) and the dead overflowError path are gone,
and OperationsFunctions.hpp with them. The unsigned-nondet name check
follows the core generator __VERIFIER_nondet_uint.
PassIR tests cover every binop (callee, type, operands, bits, line,
function) and the widths 8/16/32/64.
…rom NonDetPass NonDetPass keeps the core generators __VERIFIER_nondet_<t> (retargeting __VERIFIER_nondet_unsigned to __VERIFIER_nondet_uint per call, so later calls are still logged as unsigned) and logs each value through map2check_save_nondet_log_<t>(line, scope, type_var, slot, fn): the value is stored in an entry alloca of the C type of the library's api-deltas (bool widens to int) and type_var is the NONDET_TYPE number. The slot and its store carry map2check.runtime metadata. Assumes: __VERIFIER_assume keeps its name; Clam's nounwind verifier.assume(i1) is replaced by a zext call to __VERIFIER_assume; assume_abort_if_not and friends call it with cond != 0; a program's own __VERIFIER_assume loses its body so the library's is the only one. The library's assume unwinds, so nounwind is dropped from its declaration, from the rewritten functions and from all their call sites (RuntimeABI allowUnwind). NonDetFunctions.hpp is gone. RuntimeABI gains nonDetValueSlot, allowUnwind and kRuntimeMetadata, with RuntimeABITest coverage; PassIR tests cover the 16 types, the C names, the assume rewrites and nounwind.
When the program already declares __VERIFIER_assume nounwind, the loop predicate calls reuse that declaration. The library's assume unwinds through them, so the pass now clears nounwind on the declaration and every call (RuntimeABI allowUnwind). loop_assume.ll carries such a declaration; it also backs the NonDetPass nounwind test, since clang -O0 leaves external declarations without nounwind and assume.c could not show the fix.
…Pass Every runtime call of MemoryTrackPass goes through RuntimeABI with the core order and widths (sizes, lines and scopes are i32): - malloc/valloc/calloc/realloc/posix_memalign -> map_malloc, map_calloc, map_posix_memalign; realloc checks its old block with check_free_resolved_address (is_null_valid i16 1); - globals, allocas and alloca() -> map_alloca; a VLA -> map_non_static_alloca with its element count; - loads, stores, memset, memcpy -> check_load(ptr, line, scope, size, fn), which records the violation itself, so check_deref is gone; - stores of pointers -> map_store_pointer; - free(var) -> load *slot, skip NULL, then check_free and map_free, both (name, slot, *slot, scope, line, fn), guarded after the walk; free(expr) -> check_free_resolved_address (is_null_valid 0); - the wasm2c hooks keep their names (wasm_free takes an i64 line). Instructions tagged map2check.runtime (NonDetPass's value slots) are not tracked. The dead, type-unsafe instrumentFunctionArgumentAddress is gone. PassIR tests cover each hook's callee, type and arguments, the free guard, and the wasm mode.
Deleting its body left an empty function to the passes that run after nondet-pass in the same pipeline, and Map2CheckLibrary crashed opt on it (found by the end-to-end link). NonDetPass now renames the program's definition to an internal, unused __map2check_program_assume and sends every use to the core __VERIFIER_assume declaration, so the library's definition is still the only one. The PassIR test runs nondet-pass,map2check-library to cover the crash.
EndToEndLinkTest (Task 3.2 Steps 5 and 5b), one ctest entry per mode and input. Each input of tests/unit/pass/inputs is compiled as the frontend compiles the program (-c -emit-llvm -g -fexceptions -O0), instrumented with every pass of the mode as Caller::callPass chains them (nondet-pass, the mode's pass, map2check-library with -m2c-analysis-mode), and linked with clang-16 -fexceptions -fsanitize=fuzzer against the Rust runtime; the link must succeed with no undefined reference and no multiple definition. The modes are memtrack, memcleanup, overflow, assert, target and none. EndToEndRun.AssumeRejectionsUnwindAtO2UnderLibFuzzer builds assume_runs.c at -O2, checks that no frame the unwind crosses is nounwind, and runs 100 rejected inputs and then one accepted input through the libFuzzer driver: exit 0, 101 executions, only the accepted input prints, and no abort or panic message. target.c now defines reach_error and wasm.ll defines its allocators, so both inputs are whole programs. The library path comes from MAP2CHECK_RUST_LIB_DIR (or MAP2CHECK_RUST_SRC); without either the test is skipped.
free(var) loaded *slot a second time (%map2check.freed) for the NULL guard, check_free and map_free. The block is now the program's load, the very value free receives; it dominates the call, so it also dominates the guarded block. One load per free, as in the C runtime; under KLEE a symbolic slot no longer costs a second resolution. The PassIR test requires check_free and map_free to get that same SSA value and finds no other load of the slot up to the free.
…trumenting SV-COMP programs define library exports themselves, and the link saw two definitions (multiple definition of __VERIFIER_assert, ...). RuntimeABI now keeps the two lists and resolveProgramDefinitions(module) applies them, idempotently, as the first step of NonDetPass (first in every pipeline) and again in Map2CheckLibrary: - discarded (__VERIFIER_assume and the 16 exported __VERIFIER_nondet_*): every use goes to a declaration of the same name, so calls bind to the library (fuzzer/KLEE input, the pruning assume); the old body becomes an unused internal __map2check_program_<name> holding unreachable. This generalises 072afa6, whose __VERIFIER_assume branch moves here; - internalized (__VERIFIER_assert, __VERIFIER_error, get_current_step, get_next_step, get_current_property, set_false_result, print_all_containers_as_json, vcc_reset_meta_data): the program keeps its body with internal linkage under the same name, so AssertPass still matches __VERIFIER_assert call sites by name. The DebugInfo and RuntimeABI object libraries are now built with position-independent code; the plugins are shared objects and the lists' std::vector code needs it. Tests: PassIR checks both treatments, with the definitions before and after main; RuntimeABITest checks the lists. svcomp_defs.c and svcomp_defs_late.c join the end-to-end matrix (every mode links, 0 undefined, 0 duplicate), and EndToEndRun.ProgramDefinedExportsGiveWay- ToTheLibrary shows at -O2 under libFuzzer that input 7 is pruned by the library's assume and input 123456 reaches a branch the program's return-0 generator never would, while the internalized get_current_step still runs its own body.
The frontend links the Rust runtime (decision D1) and no bitcode of the
C runtime, WasmRuntimeStubs.bc included (the library's wasm feature
provides wasm_rt_*):
- afl/none (route B1): the -fuzzed, -witness-fuzzed and -cmplog binaries
are afl-clang-fast -fsanitize=fuzzer <hash>-result.bc
${MAP2CHECK_PATH}/lib/libmap2check.a -ldl -lpthread -lm, with the
previous -g/-O2 flags; CmpLog runs under `env AFL_LLVM_CMPLOG=1`. The
library's LLVMFuzzerTestOneInput drives __map2check_main__.
- symex (route A'): llvm-link of <hash>-output.bc with
${MAP2CHECK_PATH}/lib/map2check-klee.bc. --nondet-generator symex on an
install without that file exits with code 3 and says how to fix it; the
hybrid default skips its KLEE phase with an error message.
- Witness (Step 4b): the witness binary and the witness bitcode also link
a generated constructor that calls map2check_enable_witness(), native
for AFL++ and -emit-llvm for KLEE, both with -fexceptions.
- Crashes are replayed on the witness binary with the file as an
argument, not on stdin (D1 condition 2).
- The afl-fuzz placeholder seed is 8 bytes, the widest nondet value, so
CmpLog finds a whole operand in it (D1 condition 4); a seed directory
that already holds seeds is left untouched.
- --btree is a no-op that logs "--btree is ignored by the Rust runtime"
(provisional, decision D3).
The command builders are pure functions in caller_link.cpp, covered by
CallerLinkTest over every mode and generator, wasm, witness and CmpLog.
Also include <cstdlib> where caller_link.cpp calls getenv.
Task 4.3 measures the C runtime with --btree. EXTRA_FLAGS is appended to the per-property flags; unset, the command line is unchanged.
The gate runs each side under a container memory cap. A new oom_kill in memory.events during a task without a decided verdict is written as OOM; a decided verdict is kept and the kill is reported on stderr.
Rust (lib 44585e8) and C (f01e8c3) baselines, GENS="afl symex" REPS=5, the C --btree run on valid-memsafety (REPS=3), both sides capped at 3 GiB / 4 CPUs with KLEE --max-memory=2000. The gate fails: three C defects (property-file race under KLEE, afl OOM) and the median RSS ratio of 1.36. Proposed accepted deltas cover only budget gains and the list-ext benchmark UB.
15 symex rows: KLEE spends about 2.6 s before the first instruction on the 2.3 MB runtime module (about 1.9 s of it in --optimize); exploration is as fast as C or faster. Deleting the std backtrace symbolizer bodies halves that start-up and lowers KLEE's peak RSS from 221 to 161 MB. 2 afl rows: C's AFL++ link fails on __VERIFIER_assert and skips fuzzing, Rust fuzzes and hits AFL++'s 1 s dry-run timeout. list-ext afl: extra fuzzing that finds the target (accepted delta).
The map2check-library release archive ships three builds in lib/; the one Map2Check links is libmap2check_runtime.a (profile runtime, features libfuzzer,wasm), while its libmap2check.a is the featureless core build. With MAP2CHECK_RUST_LIB_DIR pointing at that lib/, prefer the runtime build and install it as lib/libmap2check.a, the name the frontend uses. The three cache variables now default to the environment variables of the same name, so an image can carry them. The resolved path is exported as MAP2CHECK_RUST_RUNTIME_LIB and the module is included before the tests, so EndToEndLinkTest links the same file that is installed.
Fetch map2check-library v1.1.0-rc1 (SHA-256 pinned in scripts/runtime/fetch-map2check-library.sh) into /opt/map2check-library and configure every CMake build with -DMAP2CHECK_RUST_LIB_DIR. The KLEE runtime bitcode is not in the archive: a new job builds it from the same tag (commit pinned) with rustc 1.72.1 and hands it to the Docker jobs as -DMAP2CHECK_RUST_KLEE_BC, so the symex steps keep running. Dockerfile.dev does the same: the archive in /opt/map2check-library, the KLEE bitcode built and the Rust toolchain removed, and both paths set as environment defaults for CMake. Drop the cppcheck pass over modules/backend/library: the C runtime is out of the build and stays in the tree only until it is removed.
scripts/runtime/build-map2check-klee-bc.sh matched the *build-* pattern of .gitignore and never reached the branch; it is now map2check-klee-bc.sh. cppcheck over tests/unit flags memleakOnRealloc in tests/unit/pass/inputs/memtrack.c, a PassIRTest input whose 'p = realloc(p, ...)' is the pattern the realloc instrumentation is tested on. Suppress that id for that file only.
The TestCov gate observed COVERED where expected.txt said NOT_COVERED (finding K). The cause is the runtime: the C one formatted each symbolic nondet value in uClibc's vfprintf, forking on every digit, while the Rust KLEE runtime concretizes the value before writing it (D1 condition 7), so the test vector comes out within the budget.
With --add-invariants and a .bc input the frontend still took compileCFile, so Clam never ran. test_add_invariants.sh passed anyway: it matched the name map2check_crab_assume anywhere in the scratch bitcode, and the C runtime linked into the result bitcode defines it. With the Rust runtime that definition is gone and the check failed. compileWithClam now takes the bitcode as Clam's input as is, and the test requires a call to verifier.assume or map2check_crab_assume, not just the name.
The KLEE runtime layer ran 'curl https://sh.rustup.rs | sh' as root: the toolchain was pinned, the installer was not. Download rustup-init 1.28.2 for x86_64-unknown-linux-gnu from static.rust-lang.org/rustup/archive, check it against the SHA-256 of the .sha256 file published next to it, and run it with the same options; a mismatch stops the build.
loop_reads.c checks sum == 10, which any order of its reads satisfies, so it witnesses the count of the input sequence, not its order. The README, its table and the program comment said otherwise. Note that the environment defaults of the runtime cache variables apply only on the first configure of a build directory, and raise the Valgrind job timeout from 30 to 45 minutes: its ctest step now takes about 15.
…e changelog README build section: MAP2CHECK_RUST_LIB_DIR, MAP2CHECK_RUST_SRC and MAP2CHECK_RUST_KLEE_BC, and map2check-library 1.1.0-rc1 as the minimum version. CHANGELOG: "Runtime replaced by map2check-library (Rust)".
MAP2CHECK_RUST_LIB_DIR without libmap2check_runtime.a used to fall back to libmap2check.a silently. In the release archive that name is the featureless core build, which lacks the libfuzzer and wasm entry points. The fallback now requires the archive to define LLVMFuzzerTestOneInput and map2check_wasm_malloc, as a local target/runtime build does, and configure fails with a clear message otherwise. llvm-nm-16 cannot read the members (rustc's newer bitcode), so every nm on the PATH is tried. test_rust_runtime_cmake.sh: cases for the local layout (accepted) and for a directory holding only a core build, synthetic and the release one (rejected).
baseline-rust-gate2.tsv: HEAD f7f15e3 linked against the v1.1.0-rc1 release archive and the KLEE bitcode of scripts/runtime/map2check-klee-bc.sh, afl and symex, 5 reps, same caps as gate run 1. compare.py against baseline-c-gate.tsv with deltas-aceitos.tsv: gate PASS, median wall 1.026, median RSS 1.017. The report notes one row with disagreeing reps (tree_stack symex) and the frontend exit-137 hypothesis behind its SUCCEEDED rep.
The SRC route built target/runtime/libmap2check.a through a custom command whose output, once present, was up to date: an archive left by a cargo build without the libfuzzer/wasm features was installed as is. The route is now a custom target that runs cargo on every build (cargo is incremental) and then the same symbol check as the LIB_DIR fallback, moved to cmake/Map2CheckRustRuntimeCheck.cmake (include() at configure time, cmake -P after cargo). The check now tells "no nm could read the archive" apart from "the symbol is not defined". test_rust_runtime_cmake.sh: libfuzzer-only archives (synthetic and the release one) rejected; no readable nm rejected with its own message; SRC route with a stale core archive fails after running cargo, and a rebuilt runtime archive passes with cargo run on every build. README: the SRC route also builds the KLEE bitcode when rustc 1.72.1 and llvm-dis are present.
hbgit
marked this pull request as ready for review
October 17, 2026 20:54
Owner
Author
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Migração direta do runtime C (
modules/backend/library) para a biblioteca Rust map2check-library, conforme o plano de cutover (map2check-library:docs/superpowers/plans/2026-10-15-cutover-runtime-c-map2check.md).Em draft. Task 5.1, passos 1–3 feitos (segundo
gate: PASS, ensaio de rollback, README/CHANGELOG); falta o mantenedor tirar de draft e mergear com merge commit (passos 4–6).O que muda
cmake/Map2CheckRustRuntime.cmake,MAP2CHECK_RUST_LIB_DIR/MAP2CHECK_RUST_SRC/MAP2CHECK_RUST_KLEE_BC). Versão mínima da biblioteca: 1.1.0-rc1 (README, seção de build). Um diretório só com olibmap2check.anúcleo (semlibfuzzer/wasm) agora falha no configure.RuntimeABI.hpp/.cpp); o modo de análise é escolhido em tempo de execução (map2check_set_mode).Caller::linkLLVMliga o runtime Rust: afl viaafl-clang-fast -fsanitize=fuzzer, symex via o bitcode KLEE da biblioteca; o programa é compilado com-fexceptions.--btreevira no-op com aviso (D3).tests/unit/backend-librarysai doctest.Validação diferencial (Fase 4)
scripts/cutover/run-corpus.sh+scripts/cutover/compare.py, 410 linhas por lado, 5 repetições, docker--memory 3g --cpus 4, KLEE--max-memory=2000.gate: PASS, mediana de tempo 1.011, mediana de RSS 1.081 (limite 1.36, D4).f7f15e3b, ligado aolib/libmap2check_runtime.ado releasev1.1.0-rc1(sha256 verificado) e ao.bcKLEE descripts/runtime/map2check-klee-bc.sh; afl + symex, 5 repetições; C =baseline-c-gate.tsv(o merge-base não mudou, rebase no-op).compare.py … baseline-rust-gate2.tsv --accepted deltas-aceitos.tsv:median wall ratio: 1.026 median rss ratio: 1.017→gate: PASS. Nenhuma divergência nova; nenhum delta acrescentado. Uma linha (tree_stack, symex) teve repetições discordantes (moda UNKNOWN, como no C); re-execução diagnóstica deu UNKNOWN 5/5. Detalhes emgate-report.md, seção "Gate 2".tests/cutover/deltas-aceitos.tsv(19 linhas: ganhos de orçamento, UB do benchmark list-ext, SD-20 corrida do arquivo de propriedade no C, SD-21 OOM do C no afl).tests/cutover/gate-report.md(inclui os perfis do critério 9).Rollback
Merge com merge commit;
git revert -m 1 <merge>restaura o runtime C. Tag de preservação:legacy/c-runtime-final.Ensaio (Task 5.1, passo 2, 2026-10-17): num clone descartável,
develop(f01e8c3e) +git merge --no-ff feat/rust-runtime(f7f15e3b), depoisgit revert -m 1 HEAD. A árvore resultante é idêntica à dedevelop(git diff f01e8c3e HEADvazio); repetido só em git paraf00d33e6(acrescenta a tabela e o relatório do gate 2), com o mesmo resultado. Build completo (KLEE + AFL++,-DENABLE_TEST=ON) na imagem C de develop (map2check-dev:cutover-f01e8c3e): instala de novo os.bcdo runtime C e nenhumlibmap2check.a;ctest: 10/10 passam. Nada foi publicado a partir do clone.