Repository navigation
Conversation
tests/ffi_harness.c previously exercised roughly a third of the extern "C"
surface (mostly memtrack + a couple of nondet/overflow variants), leaving
the M2 acceptance criterion ("100% dos exports sob ASan/UBSan") unmet in
the letter even though ffi_guard() already wraps every export uniformly.
Adds hostile-input (pre-init, null/garbage) and well-formed (post-init)
calls to every remaining symbol: set_false_result, get_current_property/
step, print_all_containers_as_json, vcc_reset_meta_data,
map2check_set_memcleanup/set_null_is_valid, all six
map2check_save_nondet_log_*, basic-block tracking, the full overflow binop/
shift family, map2check_check_mem_endprog, and the ten missing
__VERIFIER_nondet_* variants.
Declares by hand the macro-generated symbols cbindgen's header omits
(nondet_ffi!/overflow_ffi_binop!/overflow_ffi_shift! expansions aren't
picked up by cbindgen), matching the exact signatures in rust/src/ffi.rs.
Verified: gcc -fsyntax-only -Wall -Wextra clean; scripted diff confirms
all 53 exported symbols (40 in ffi.rs + 13 in nondet/libfuzzer.rs) are now
invoked. Not verified under clang+ASan/UBSan locally (no clang on this
machine) — that still needs a CI run after push.
Co-authored-by: hbgit <1494322+hbgit@users.noreply.github.com>
All CI checks pass (build_and_test × 2, GitGuardian). Local verification complete: 45 Rust unit tests pass, C FFI harness runs clean under ASan/UBSan, Docker build succeeds.
Resolve the five conflicting paths between M3 and the post-PR-#2 base. Base-branch signatures are canonical for the three FFI symbols both branches implemented independently; PR #3's signature-neutral semantics (dynamic VLA entry, pointer-width function-address entry, FreeResolvedChecker, char as i8) are preserved. C tests adapted to the canonical ABI; PR #3's SV-COMP exports restored to the FFI harness. Co-Authored-By: Claude Code <noreply@anthropic.com>
The merge took the base's Cargo.toml, which removed PR #3's [profile.release] panic = "abort" (dropped in 860368c), but kept three in-tree documents written against it: the __VERIFIER_assume design note in rust/src/nondet/libfuzzer.rs, the accepted-risk section of docs/api-deltas.md, and the retry-loop note in .github/workflows/CI.yml. Each is reworded to the reason that still holds: the LibFuzzer entry point is extern "C", so a Rust panic must not cross the FFI boundary regardless of the release profile's panic strategy, and there is no portable way to unwind out of an arbitrarily deep call stack back to LLVMFuzzerTestOneInput. Documentation only -- no behavior, ABI or signature change. Found by the post-merge whole-branch review. Co-Authored-By: Claude Code <noreply@anthropic.com>
Implementação do M3
Audit every verifiable item of docs/plano_map2check_library_rust.md (M1-M8 issues, deliverables, acceptance criteria, DoD and the 7 global readiness criteria) against origin/feature/rust @ 0f28571, with raw command evidence under audit/evidence/. Pending and partial items were filed as issues #25-#29 and as comments on #8, #9, #11, #13, #15 and #16; milestones and labels from the plan were created. audit/create_issues.sh is idempotent (dry-run by default).
Single scripts/coverage.sh shared by CI and the Dockerfile test stage; the lcov/html report is uploaded as the 'coverage' artifact. The Dockerfile no longer masks tarpaulin failures with '|| mkdir -p /coverage'. Refs #25.
ci: enforce 80% tarpaulin coverage gate outside ffi*.rs
ci: protect feature/rust and master with required CI (#26)
Signed-off-by: Herbert Rocha <herberthb12@gmail.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- catch the .clangd/ index directory, not only a .clangd file - run_libfuzzer_test.sh drove the removed CMake build/a.out flow; remove it and guard it - read git ls-files -z so quoted names are checked; fail on grep errors Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
chore: remove C-era dead artifacts (#27)
…28) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…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.
Prepare the library to replace the Map2Check C runtime (1.1.0-rc1)
test: port Map2Check C runtime unit assertions to Rust
release: 1.1.0-rc1
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.
Promove develop para main para o release 1.1.0-rc1 (docs/release.md, passo 4). Inclui o cutover do runtime (#41), as asserções portadas dos testes C (#42) e a preparação do release (#43).