Repository navigation
Prepare the library to replace the Map2Check C runtime (1.1.0-rc1) - #41
Merged
Merged
Conversation
…hs, overflowError, termination notes)
…pLog gap, real symex build, MSRV cost)
A memory check that found the access safe reset the result to OK, which erased any earlier violation, including one recorded by set_false_result. The C runtime of Map2Check develop ends the process on the first violation (map2check_error -> map2check_exit -> abort), so the first violation is final there. AnalysisState::set_false now ignores every violation after the first, and the memory checks no longer reset the result before checking. The analysis keeps running; ending the process belongs to a later task. Invert the pinning test into sd03_safe_check_keeps_earlier_violation, add sd03_later_violation_does_not_overwrite_first, split the tests that chained independent violations, flip the harness case, mark SD-03 fixed (new 'fixed' classification) and update the integration guide.
map2check_check_free_resolved_address treated an address with no heap record as a safe free, while map2check_check_free reported MEMSAFETY_FREE for it. The C runtime of Map2Check develop uses is_invalid_free (ListLog.c:95-118) on both free paths, and it returns true when no row points to the address. is_invalid_free_resolved now lets the most recent heap record (allocation or free) decide and reports an address with none as invalid. Invert the pinning tests, add sd06_untracked_free_is_invalid and a stack-slot case, mark SD-06 fixed and update api-deltas and the ABI mapping row.
map2check_map_non_static_alloca marked its record dynamic, so a VLA was reported as MEMSAFETY_MEMCLEANUP at end of program, and it took size in bytes. The C runtime of Map2Check develop forwards to map2check_alloca with size * size_of_primitive (AnalysisModeMemtrack.c:368-372), a static heap_log slot that the leak check never sees. The export now registers a static slot of size * size_primitive bytes and drops the record when that product overflows. The signature is unchanged. Replace the three pinning tests with sd12_vla_is_not_a_leak_and_size_is_elements and companions, mark SD-12 fixed and update api-deltas and the ABI mapping row.
map2check_check_load accepted an access to a freed block because the older malloc record still covered the address. In the C runtime of Map2Check develop, the allocation log keeps one row per address, updated in place on malloc and free (AnalysisModeMemtrack.c:313-317, :360-363), so only the latest event counts (AllocationLog.c:127-148). is_invalid_address now lets the latest heap event per block address decide, keeps stack slots valid and ignores pointer stores. Add tests for use-after-free (load and deref), reallocation at the same address, a smaller reallocation, range boundaries and a pointer store after free.
map2check_check_free_resolved_address only checked, while map2check_free_resolved_address in the C runtime of Map2Check develop also marks the block freed (AnalysisModeMemtrack.c:178-182). The pass uses this path for realloc and for frees of a non-load value, so a moved realloc gave a false MEMSAFETY_MEMCLEANUP, and use-after-free and double free through this path went unreported. The export now records a free event when the check passes (never for NULL or a failed check). Add tests for a realloc-style sequence, a double resolved free and a load after a resolved free. Update ABI mapping row 27 and document the asymmetry with map2check_check_free. Also add SD-13 (intentional): a block freed without ever being stored through a tracked pointer is a valid free here, while develop reports FALSE_FREE because is_invalid_free scans only list_log. Correct SD-06, which overstated parity, and document vcc_reset_meta_data as a host/test-only export that clears a violation by design.
Keep the options in a configuration that init and reset do not clear. The end-of-program leak check now always runs and reports memtrack or memcleanup by option, as the develop C runtime does (SD-04).
Add map2check_set_mode(AnalysisMode) and keep the mode in the run configuration, so init and reset keep it. Each analysis_init, analysis_destroy, analysis_is_program_correct and check gate of the develop AnalysisMode*.c files becomes a match in analysismode/mode.rs. With no mode set every check stays active, as before. Add map2check_reach_target, which records Reachability (develop TARGET-REACHED) and returns. Append Assert and Unknown to ViolatedProperty and report failed asserts as Assert.
map2check_set_mode now takes an int32_t. A value outside 0-5 is ignored with a diagnostic instead of being undefined behaviour. The header still declares enum AnalysisMode for the values. Memcleanup mode now reports a leak only when the last leaked block is still referenced by a pointer variable, as develop does. The allocation and list logs are replayed from the memtrack entries. Memtrack mode already matched develop. Remove the unused MemCleanupChecker.
…p2Check frontend (#19, #14) With an analysis mode set, the library now ends a run as the C runtime of Map2Check develop does: the first violation writes the property files and aborts, and map2check_success() writes NONE, runs the end-of-program verdict and returns. map2check_enable_witness() adds the witness files (track_bb_log.st, heap/allocation/list logs, klee_log.csv and map2check_checked_error). map2check_init() removes stale property files. Without a mode nothing is written and nothing aborts. Golden tests compare every file byte for byte with tests/legacy_golden. The JSON report stays as an additional channel, pinned by a snapshot. New semantic deltas: SD-16 (map2check_property__unknown kept on purpose) and SD-17 (logs rebuilt from this library's records).
…n as UNKNOWN (#19) With a mode set no export writes to stdout, as in develop: map2check_success, print_all_containers_as_json, a failing map2check_is_valid_assert and __VERIFIER_error print the JSON report only when the mode is unset. The report is serialised under the state lock and written after it, and a stdout error only goes to stderr, so it can no longer drop a verdict or skip the abort. When the state lock is poisoned at the end of a run, the run now ends as develop's UNKNOWN: the NONE already written is removed, map2check_property__unknown is written and the process aborts. The golden tests check that the child's stdout holds only the markers. The C harness checks a file's absence with access().
…n by zero (#13) Add map2check_binop_{add,sub,mul,div,rem}_signed(a, b, bits, line, fn), the core targets of develop's map2check_binop_{add,sub,mul,sdiv,srem} (AnalysisModeOverflow.c:110-276): 64-bit predicates, then the range of the operation's width; MIN / -1 and MIN % -1 overflow; a zero divisor reports the new ViolatedProperty::DivByZero (10), written as FALSE-DIVBYZERO to map2check_property only (PropertyGenerator.c:98-102). Gated like the other binops. Golden DIVBYZERO captured from develop.
Add map2check_map_posix_memalign(ptr_address, size), the core target of develop's map2check_posix (AnalysisModeMemtrack.c:327-333): reads the block from *ptr_address, records it as map2check_map_malloc and records the store into *ptr_address with the scope, line, name and function develop passes. Golden POSIX-MEMALIGN captured from develop.
…ames it (#13, #19) map2check_check_free and map2check_map_free take (name, var_address, ptr, scope, line, fn): var_address is the slot develop's map2check_free receives (MemoryTrackPass.cpp:818), ptr stays the block the checks are keyed on. The FREE row of list_log.csv and the memcleanup verdict now use the real variable, and a failing check keeps the row develop appends before it checks (AnalysisModeMemtrack.c:346-358). Golden FALSE-FREE now covers the failing map2check_free path; the old scenario is kept as FALSE-FREE-RESOLVED. SD-17 loses its two free cases.
…and free exports Only the nondet rows (Task 2.5b) and the wasm rows (Task 2.8) are still missing from include/map2check.h.
) Add map2check_save_nondet_log_{unsigned,ulong,uchar,short,ushort,bool, size_t,loff_t,sector_t,pointer,pchar}, each taking a pointer to the value in the C type develop's NonDetGenerator.h gives the family, with the existing (line, scope, type_var, value, function_name) signature. klee_log.csv now matches develop for every type: the enum NONDET_TYPE number of the export and the value as NonDetPass.cpp hands it to the C int wrapper (CreateIntegerCast with isSigned = false, so narrow types are zero-extended and wide ones truncated; ptrtoint for addresses), printed with %u for UNSIGNED and %d otherwise. A char -3 is therefore logged as 253, as develop does; golden.h passed it sign-extended, which no pass emits, so the shared goldens are regenerated and only that row changes. The new golden NONDET-TYPES, captured from develop in map2check-dev:cutover-f01e8c3e, logs one value of each type.
Condition 3 stays NOT MET with its numbers and is replaced by gate 4.2's criteria (median wall-time ratio <= 1.10, no new timeouts). Condition 4 is mitigated by a frontend seed of at least 8 bytes (Task 3.3, rechecked at gate 4.2). New condition 11: the program is compiled with -fexceptions (Task 3.2). The plan gets the matching steps in Tasks 3.2 and 3.3, and the spike write-up records corpus_count and the B2 queue entries behind the condition 4 analysis.
The symex runtime (D1 route A') builds rust/src with rustc 1.72.1, whose LLVM 16 writes bitcode KLEE 3.1 reads (condition 5): - state.rs: OnceLock::get_or_init instead of LazyLock (unstable in 1.72); Mutex::clear_poison stays in the normal build and is compiled out under feature "klee", whose panic = "abort" profile cannot poison the lock. - memtrack: map_or(true, ..) instead of Option::is_none_or (1.82). - The three HashSets use fixed SipHash keys (memtrack::FixedHashSet): RandomState seeds itself through a weak getrandom symbol, which under KLEE is an invalid function pointer. The sets only answer membership. - Cargo.toml: the empty `klee` feature leaves the main manifest; it belongs to the KLEE build's own manifest. Here `--all-features` would enable it next to `libfuzzer` (and drop clear_poison from the tests). The value is declared for check-cfg instead.
tests/klee_paths.sh builds the symex runtime bitcode, links each program of tests/klee/ to it with llvm-link-16 and runs KLEE 3.1 with the frontend's flags, in docker (tests/klee/Dockerfile: the Map2Check dev image plus rustup 1.82.0 and 1.72.1): - prog.c: the D1 spike's program as the passes leave it; 2 completed paths and a ktest with x = 42; - reach.c, range.c, json.c: the witness nondet log and the JSON report must not fork KLEE (D1 condition 7); - deref.c: KLEE finds the off-by-one read, the property file says FALSE-DEREF; - layout.c: the error path's ktest, turned into a seed as the frontend's exportKleeVectorsAsSeeds does, replayed by the Rust libFuzzer reader, reaches the same error (D1 condition 9). With DEVELOP_SRC it also runs the programs on develop's C KLEE runtime and prints both path counts. It fails until the runtime exists.
D1 route A': the map2check-library sources, built by rustc 1.72.1 as one LLVM 16 bitcode module that llvm-link-16 joins to the analysed program for KLEE 3.1. - klee/Cargo.toml: second manifest (own [workspace], build = false, no dev-dependencies, rust-version 1.72, feature klee, dependency caps, release profile with panic = abort, fat LTO, codegen-units = 1) and its own Cargo.lock v3 from the MSRV-aware resolver. - rust/src/nondet/klee.rs: __VERIFIER_nondet_<t> -> klee_make_symbolic with sizeof(type) bytes, objects named non_det_<t> as develop's NonDetGeneratorKlee.c names them; __VERIFIER_assume -> klee_assume; __VERIFIER_error/_assert as in the libFuzzer generator (shared body); main -> __map2check_main__; pchar capped at 4096 like the AFL++ reader. - Concretisation before output (D1 condition 7): prepare_for_output replaces nondet values and memory-record addresses/sizes with klee_get_value_* values, constrained with klee_assume, before the witness logs and the JSON report are formatted. No-op elsewhere. - scripts/build-klee-runtime.sh <out.bc>: the exact build, checks the rustc flags and LLVM 16, opt-16 --strip-debug (condition 6), lowers the vector/x86 intrinsics of the precompiled std that KLEE 3.1 cannot execute (scripts/klee-lower-intrinsics.py), reads the result back with llvm-dis-16 and checks the exported and imported symbols. - The klee module stays out of the C header (cbindgen:ignore); the export checklists cover klee.rs. tests/klee_paths.sh passes; path counts equal develop's C runtime on prog/reach/deref/layout and lower on range (1+1 vs 1+7).
New job klee_runtime on ubuntu-24.04: installs LLVM 16 (apt llvm-16) and rustc 1.72.1, runs scripts/build-klee-runtime.sh against klee/Cargo.toml with its own lockfile (--locked), checks the bitcode exists and that llvm-dis-16 reads it, runs cargo-deny on klee/Cargo.lock and uploads the .bc. It is the guard of D1 condition 5: clippy on 1.82 does not see std API newer than 1.72. KLEE itself does not run here (its image is Map2Check's dev image); tests/klee_paths.sh runs locally and in Map2Check's CI (Task 3.4).
…ns 5, 6, 7 and 9 docs/klee-feasibility.md: the product (second manifest, lockfile, feature klee, build script, test, CI), the generator's semantics against develop's NonDetGeneratorKlee.c, the evidence of tests/klee_paths.sh (path counts Rust vs develop C), the findings (vector intrinsics of the precompiled std, RandomState under KLEE) and the limitations. decisoes.md: conditions 5, 6, 7 and 9 (KLEE side) marked ATENDIDA with their evidence. TODO.md: the KLEE gate item is done.
develop's __VERIFIER_error (Map2CheckFunctions.c:57-59) and __VERIFIER_assert (AnalysisModeAssert.c:25-27) do nothing; the passes report through map2check_target_function and map2check_assert. Both Rust generators recorded REACHABILITY and aborted in every mode, with no property file. Under KLEE's --exit-on-error-type=Abort that ended the exploration before the real violation of a memory or overflow task, and under the fuzzer it was a crash with no property. With an analysis mode set, both now return and record nothing, in the libFuzzer and KLEE generators (shared record_verifier_error). With the mode unset (direct API users) they keep recording REACHABILITY and aborting. Tests: libFuzzer unit tests (memtrack: __VERIFIER_error then an invalid load gives MemsafetyDeref; target: only map2check_reach_target reports) and tests/klee programs vererr_deref.c (FALSE-DEREF on both runtimes) and vererr_target.c (no abort, NONE, 2 paths on both). SD-08 rewritten: its legacy paragraph described map2check_error, not __VERIFIER_error.
- klee-lower-intrinsics.py: after the rewrite, every intrinsic still declared must be in KLEE 3.1's list (the `case Intrinsic::` labels of Executor.cpp and IntrinsicCleaner.cpp at v3.1), with bitreverse as a justified exception; anything else fails the build instead of killing a KLEE path at run time. The hand-written rewrite stays the only mechanism: -expand-reductions covers only the reduce family and lives in the legacy pass manager. - build-klee-runtime.sh runs the lowering's self-tests before using it: lli-16 equivalence on tests/klee/lower-intrinsics.ll (now with reduce.add.v2i64, which the runtime uses) and rejection of tests/klee/unknown-intrinsic.ll (llvm.masked.load). It builds in a temporary directory, removes <out.bc> first and moves the result only at the end, so a failure leaves no bitcode; klee_paths.sh checks that. - CI klee_runtime: clippy 1.72.1 on the klee build (the only lint of nondet/klee.rs) and lli-16 for the self-tests. - klee.rs: main allows not_unsafe_ptr_arg_deref (argv is only passed on).
api-deltas: __VERIFIER_error/_assert are libfuzzer and klee exports and do nothing with a mode set (SD-08); new section on the KLEE generator and its differences from develop's (naming, float, pchar cap, concretisation). klee-feasibility: __VERIFIER_error row, the vererr programs and counts, the intrinsic allowlist and self-tests, the clippy step.
The wasm_rt_* stubs of WasmRuntimeStubs.c, w2c_wasi__snapshot__preview1_proc_exit and map2check_wasm_malloc/free/check_access (AnalysisModeMemtrack.c:385-430), with wasm_rt_memory_t and wasm_rt_funcref_table_t mirrored from wabt 1.0.41. The layout test compares them with wasm-rt.h when WASM_RT_INCLUDE is set.
…sm-rt.h layout in CI
Add the 1.1.0-rc1 changelog section with the breaking changes, document the runtime-profile and KLEE bitcode build commands, and ship the runtime-profile library (features libfuzzer,wasm) in the release archive.
cbindgen 0.26 pulled clap 3 and atty (RUSTSEC-2021-0145). 0.28 builds with rustc 1.82 and, without its default clap feature, pulls neither. 0.29 emits the two enums in another order, so it is not used. build.rs folds the two-space closing #endif that 0.28 writes back to one space; the generated header is byte-identical to the one from 0.26.
Map2Check's --wasm mode with the symex generator stopped in KLEE with "failed external call: wasm_rt_is_initialized". The KLEE manifest now has the wasm feature and build-klee-runtime.sh builds with --features klee,wasm. tests/klee_paths.sh runs a wasm2c-lifted module against it and expects OVERFLOW at line 0, the verdict of develop's C runtime (SD-19).
… rename Under KLEE the forked states share the real file system and std::fs::write truncates and writes in separate external calls, so one state could empty map2check_property after another wrote its violation. Every legacy file is now written to a temporary file of the same directory and renamed over the target. Names, contents and write order are unchanged. Adds a reader-race test, a rename test and a multi-state KLEE case.
.cargo/config.toml added -C instrument-coverage to every cargo build in the repository, including the shipped runtime profile and the KLEE bitcode. Under KLEE the counter update in each basic block cost about a third of the runtime's instructions on list-ext. cargo tarpaulin --engine llvm adds the flag itself, so the coverage gate does not need the file. build-klee-runtime.sh now fails when the crate is compiled with instrument-coverage (from RUSTFLAGS or a config file).
is_invalid_address built a SipHash set of block addresses on every checked load. Under KLEE that was about 95% of the runtime's instructions on list-ext. It now scans newest first and, for a covering heap block, checks that no newer heap event has the same address. The result is the same: a randomized test compares it with the set-based version.
Every checked load and store built a VccContext that copied the function name into an Arc<str>. No checker reads the context, so the copy was pure cost (a malloc, a memcpy and a free per call under KLEE). The context now borrows the name. CHANGELOG records the KLEE throughput work.
develop's map2check_malloc tests the block first (AnalysisModeMemtrack.c:305-311), so a failed malloc ends the run as UNKNOWN whatever its size. The Rust runtime dropped calls with a negative size first (SD-09). The pass truncates the size to int, so malloc(4 * n) over 2 GiB, which KLEE answers with NULL, reaches the runtime as NULL with a negative size: that state was dropped and ran on, and KLEE bound the next malloc of the same symbolic size to a concrete 2 GiB object. On sv-benchmarks lis_unsafe (symex) this took KLEE to 4.4 GB RSS, against 170 MB with develop's runtime. map2check_map_malloc and map2check_map_calloc now test the block first. A non-NULL block with a negative size is still dropped. tests/klee/hugemalloc.c reproduces the lis_unsafe shape in tests/klee_paths.sh.
…r states leave In the frontend run other KLEE states also write property files (the n == 0 path ends with NONE), so the absence of map2check_property proved nothing. The check now reads n from the abort's ktest and requires 4 * n to be over 2^31, and the program frees its blocks so no state ends as FALSE-MEMTRACK.
…nd D5 SD-20 (C-BUG-property-race): the C runtime truncates the shared map2check_property from other KLEE states; the Rust library writes through a temp file and rename. SD-21 (C-BUG-oom-afl-nondet): the C NonDetLog grows across AFL++ persistent iterations until the 3 GB cap; the cause is read from the source, not profiled. decisoes.md gains D2 (port wasm, plan recommendation, executed in 2.8 and 2.8b, formal approval pending) and D5 (no compatibility layer, user decision of 2026-10-15), and a measured note under D4.
The panic hook drags gimli, addr2line, miniz_oxide, rustc_demangle and backtrace_rs into the fat-LTO module: 48% of its IR, which KLEE loads and re-optimises on every symex run. scripts/klee-stub-symbolizer.py turns their bodies (and std's backtrace printer) into abort stubs after --strip-debug, keeping bodies that rustc merged with code the runtime still reaches, and globaldce drops what only they used. A self-test fixture runs under lli-16 first and a guard fails the build if a symbolizer body is left. The module goes from 125829 to 52590 instruction lines and 2.3 MB to 1.2 MB; KLEE on byte_add_bug from 3.1 s / 221 MB to 1.3 s / 156 MB. llvm.bitreverse is gone, so klee-lower-intrinsics.py accepts no exception. tests/klee_paths.sh checks the size bound and that a panic still ends its path with a KLEE error, with and without RUST_BACKTRACE.
klee-stub-symbolizer.py never walked into, and always stubbed, any function matching the printer pattern. That pattern also matches the drop_in_place of a _print_fmt closure, a plain buffer drop rustc may merge with a String drop; had live code called it, every format! would abort under KLEE, and --check, which ran the same walk, would not have seen it. The walk now stops only at std::sys_common::backtrace::print, the call the default panic hook makes when a backtrace is asked for; every other printer function is an ordinary candidate, kept when live code reaches it. --check also fails when live code reaches a stub. The fixture gains a printer-named drop that main calls (the old script stubbed it: lli returned 134), and stub-symbolizer-live.ll must be rejected by the guard. The runtime module is byte-identical: 142 stubbed, 2 kept, 52590 lines.
The golden tests read tests/legacy_golden and the integration tests read docs/, CHANGELOG.md and the Dockerfile itself, none of which the test stage copied, so the CI docker build failed since 1.1.0-rc1.
Merged
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
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.
Resumo
Prepara a
map2check-librarypara substituir o runtime C do Map2Check (develop,modules/backend/library) e sobe a versão para 1.1.0-rc1. Plano:docs/superpowers/plans/2026-10-15-cutover-runtime-c-map2check.md. Decisões:docs/cutover/decisoes.md. A D1 foi aprovada com mitigação em Rust para o AFL++.Não há camada de compatibilidade (D5): a biblioteca exporta só a API núcleo. Os passes do Map2Check vão emitir os nomes de
docs/cutover/abi-mapping.tsv. Para gerar a matriz, rodescripts/symbol-matrix.shcontra odevelopdo Map2Check; ela sai com 0.Mudanças principais
map2check_initzera o estado a cada chamada (Reset analysis state between analyses and fuzzing iterations #9).ffi_guard, e a política de panic está documentada (Prevent unhandled failures from crossing the FFI boundary #8).runtimecompanic = "unwind".map2check_set_mode(int32)emap2check_reach_target.Assert,UnknowneDivByZero, acrescentadas ao fim do enum sem mudar os discriminantes existentes.map2check_property*,track_bb_log.ste os CSVs, byte a byte iguais aos do develop (golden files capturados do runtime C).map2check_enable_witness(), grava também os arquivos de witness.map2check_binop_*_signedcom largura de bits.map2check_map_posix_memalign.check_freeemap_freerecebem o endereço da variável ponteiro.klee_log.csvigual ao do develop.NonDetGeneratorAFL.c, inclusive o wrap de entradas curtas.LLVMFuzzerTestOneInputdescarta a entrada sem encerrar o processo. Isso exige que o programa analisado seja compilado com-fexceptions; o CI testa o harness em-O2.klee/, com rustc 1.72.1, Cargo.lock v3 próprio escripts/build-klee-runtime.sh(bitcode LLVM 16, LTO fat, intrínsecos rebaixados e checados contra uma allowlist).tests/klee_paths.sh.wasmcom os stubswasm_rt_*emap2check_wasm_*, com a mesma semântica do develop.default-features = false) para remover oatty(RUSTSEC-2021-0145); o header gerado é idêntico.Mudanças incompatíveis
Estão listadas no
CHANGELOG.md, na seção1.1.0-rc1. Em resumo:check_freeemap_freeganharam o parâmetro do endereço da variável ponteiro;set_moderecebeint32_t;Verificação
cargo fmt --checkecargo clippy --all-targets --all-features -- -D warningspassam.cargo test --all-featurespassa; a cobertura é de 88,8% (o gate é 80%).cargo deny checkpassa na raiz e emklee/.-O2, com e sem-fexceptions, e os programastest/*.ctambém.tests/klee_paths.sh(em Docker) passam.scripts/symbol-matrix.shsai com 0.Cada task do plano teve revisão própria.
Próximos passos (fora deste PR)
maine tagv1.1.0-rc1(docs/release.md).feat/rust-runtime: CMake, passes, frontend e CI. Depois disso vem o gate diferencial contra a baseline do runtime C.