Repository navigation
Conversation
…d Map2Check Restrict gh/git remote actions to explicit requests, keep all changes in this repository, and require the Map2Check copy used by integration tests to live unversioned under vendor/map2check/ (now ignored by git).
…to develop Mark the Map2Check-side steps of the cutover plan (Task 5.1 steps 5-6, Tasks 6.1-6.4) as maintainer-owned and add the agent's local tasks: 5.3 (read-only Map2Check copy under vendor/map2check/ for the gate), 5.1 step 7, 6.0 (local precondition check) and 6.4a (this repository's docs). Require the integration-test copy of Map2Check to come from the develop branch, in the plan and in the mandatory agent rules.
… runtime The merge of Map2Check PR #76 (a0f8b9cd) left develop with a force push on 2026-10-22, so the old cutover plan is superseded. The new plan builds the 21 bitcode modules Map2Check develop links, from Rust, and proves them against the C runtime with a differential gate, without changing Map2Check.
…_handle in the link matrix
Task 2.1 of the drop-in plan: the symbols of Map2CheckFunctions.bc, TrackBBLog.bc and PropertyGenerator.bc that have a consumer outside the C runtime, with the C signatures and the behaviour of develop's .c files. - map2check_init(int) and map2check_success() take the C signatures; map2check_track_bb, map2check_target_function, map2check_error, map2check_exit, map2check_destroy, map2check_get_current_step, map2check_next_current_step and write_property are new exports. - The witness entry points __m2c_rt_witness_generate_aux_files and __m2c_rt_witness_generate_confirmation_file implement WitnessGeneration.c for the IR forwarders of D7 (MAP2CHECK_SEED_REPLAY included). - The C-only helpers (write_property_<x>, trackbb_new_row, is_in_tracked, trackbb_log_to_file) stay private, per SD-22, and are tested. - ViolatedProperty takes the C enum values; pending-enums.txt loses its marker and check-signatures.sh treats an aligned enum as one type, so write_property conforms. - map2check_init no longer removes property files of an earlier run, as the C runtime. - pending.txt loses map2check_init, map2check_target_function and map2check_track_bb; the map2check_assume family waits for nondet_assume (Task 3.1).
…witness wiring into Task 3.1
Task 2.2 of the drop-in plan: the NonDetLog.bc side of the C runtime ABI. - The 23 map2check_nondet_<t> exports of NonDetLog.h (u8, u16, u32, memory_byte, longlong and ulonglong included), nondet_log_init and nondet_log_destroy take the C signatures and append to a C-shaped log (nondet::c_log) that takes and advances the C step counter. - __m2c_rt_nondet_log_to_file writes klee_log.csv byte for byte as NonDetLog.c does (hand-made decimals, %lf, %.9g), for the KLEE generator IR of D7. nondet_log_to_file, new_nondet_call, the append helper, the getter and the nondet_log global stay private (SD-22). - The none generator needs no Rust entry point: it is pure IR (Task 3.1). - The log of map2check_save_nondet_log_<t> and the JSON report are unchanged. - pending.txt loses the 22 map2check_nondet_* symbols.
- The witness path feeds the legacy nondet rows through nondet::c_log, the only klee_log.csv formatter; function names are cut at 35 bytes as in C. - __m2c_rt_nondet_log_len/get_i64/set_i64 let the KLEE IR pin the rows as NonDetGeneratorKlee.c does; docs state what the IR must do before __m2c_rt_nondet_log_to_file. - CNondetCall keeps the name in a fixed [u8; 35]; abi-mapping gains the missing nondet rows; api-deltas records the NULL name and the witness difference.
Copy spikes/d7-layout/scripts/gen_ll.py to scripts/runtime-ir/gen_ll.py with only the approved A-fwd strategy, and bring its unit tests along. The spike copy is unchanged. - Parameters and returns of char, signed char and short get signext, unsigned char and unsigned short zeroext, and _Bool becomes zeroext i1, as clang-16 lowers them for x86_64 SysV (D7 inherited finding 4). The attribute is on definitions, declarations and call sites. A test compiles every generated signature with clang and compares; it caught get_next_input_from_afl, which returns uint8_t. - --module <Module> writes a single module, byte for byte what the full run writes for it. Output is deterministic (tested). - IMPLEMENTED lists only entry points the Rust core exports (tested against rust/src/ffi.rs): the witness forwarders. The spike's assert and overflow forwarders are stubs until their tasks.
The C names of AnalysisModeOverflow.c (analysis_*, map2check_binop_*,
overflowError) are defined only by the generated IR module
AnalysisModeOverflow.ll (gen_ll.py --module AnalysisModeOverflow), which
forwards each one to a Rust core entry point __m2c_rt_overflow_<name> (D7,
A-fwd). libmap2check.a never defines them, since every mode defines
analysis_*.
- __m2c_rt_overflow_map2check_binop_{add,sub,mul,sdiv,srem}: the checks of
AnalysisModeOverflow.c:197-276 (SignedBinop), OVERFLOW or FALSE-DIVBYZERO,
with no mode gate. With the mode selected, the property files are written
byte for byte as PropertyGenerator.c writes them and the run aborts.
- The _uint binops are no-ops, as in C (:219-248).
- __m2c_rt_overflow_overflowError records OVERFLOW.
- __m2c_rt_overflow_analysis_init selects the overflow mode. The C body
is empty, because linking the module is what picks the mode.
is_program_correct returns 1; destroy and the aux witness hook are
empty. divisionByZeroError and unknown_not_supported stay private
(SD-22).
- Tests pin the C tag and the property text at INT_MAX + 1, INT_MIN - 1,
INT_MIN / -1, x % 0 and UINT_MAX + 1. The C goldens OVERFLOW and
DIVBYZERO are matched through the new entry points.
- scripts/runtime-ir/test-overflow-link.sh generates the .ll,
syntax-checks it with clang and links a C driver against the release
staticlib to show that every forwarder reaches the core. It also checks
that the staticlib defines none of the module's C names.
- CI runs the generator tests and the link test, and passes the .ll to
runtime-abi-coverage.sh. pending.txt loses the 8 map2check_binop_* and
overflowError.
The legacy map2check_binop_*_signed/_int exports are unchanged (Task 2.10).
…eader Review of Task 2.3, round 1. - The KLEE and AFL modules declared __m2c_rt_nondet_log_to_file as void, but the core returns char (signext i8). They now declare and call it as signext i8. - KLEE's nondet_generate_aux_witness_files called __m2c_rt_nondet_log_value, which the core does not export. It now uses the core hooks __m2c_rt_nondet_log_len/_get_i64/_set_i64: NonDetGeneratorKlee.c:33-62 with the 1024-row skip, then klee_get_value_i64, klee_assume of the equality, and the value written back before nondet_log_to_file. - New generator test: every @__m2c_rt_* that any generated module declares or calls must be a prototype of include/map2check.h, and its declaration and calls must match what clang emits for that prototype (D7 finding 4). It catches both bugs above. - Placeholder defines are marked `; m2c-stub`; the empty functions of WitnessGenerationNone.c are not. runtime-abi-coverage.sh no longer counts a marked define as delivered, and its test covers this. - api-deltas: a NULL function name is written as "" where C/glibc prints "(null)". - CI: drop the second cargo build in the coverage step. - Fix the RtSignedBinop/RtUnsignedBinop citations to point at the C function bodies.
The C names of AnalysisModeAssert.c and AnalysisModeNone.c (analysis_*,
map2check_assert, __VERIFIER_assert) are defined only by the generated IR
modules AnalysisModeAssert.ll and AnalysisModeNone.ll, which forward to Rust
core entry points __m2c_rt_assert_* and __m2c_rt_none_* (D7, A-fwd).
libmap2check.a never defines them.
- __m2c_rt_assert_map2check_assert: AnalysisModeAssert.c:18-23. Condition 0
records ASSERT; with the mode selected, map2check_property and
map2check_property_assert are written as PropertyGenerator.c:92-96 and the
run aborts.
- __VERIFIER_assert is an empty function in the IR (AnalysisModeAssert.c:25-27),
unmarked, with no core entry point. The legacy export stays until Task 2.10.
- __m2c_rt_{assert,none}_analysis_init select the assert and none modes. The
none module serves reachability and cover-branches; with it,
map2check_target_function writes the TARGET-REACHED property
(PropertyGenerator.c:81-85) byte for byte and aborts.
- analysis_is_program_correct is 1 in both, destroy and the aux witness hook
are empty.
- scripts/runtime-ir/test-assert-none-link.sh generates both modules, checks
them with clang and links a C driver against the release staticlib. CI runs
it and passes both .ll to runtime-abi-coverage.sh. pending.txt loses
map2check_assert.
WasmRuntimeStubs.ll defines the 10 C names wasm2c output calls: nine wasm_rt_* forward to the new __m2c_rt_wasm_* core entry points, and w2c_wasi__snapshot__preview1_proc_exit is an empty define, as in WasmRuntimeStubs.c. Adds the host link test and wires it into CI and the coverage step.
Adds a relocation-based check that no code in the release staticlib targets a name a generated IR module defines, with a fixture test, and tidies the wasm rows of api-deltas and the SD-19 trap note.
D6: libmap2check.a exports exactly the names of the C runtime of Map2Check develop that the core modules own (Map2CheckFunctions, TrackBBLog, NonDetLog, PropertyGenerator; minus c-only and IR-defined names) and the __m2c_rt_* core entry points the generated IR modules forward to. scripts/check-export-set.sh (with a fixture test, in CI) fails on anything else. - The 1.x core API (map2check_set_mode, map2check_reset, print_all_containers_as_json, map2check_map_*, map2check_check_*, map2check_save_nondet_log_*, the 1.x binops...) is no longer exported; it stays Rust API for the tests. The legacy check_deref, wasm_* and wasm_rt_* exports are gone; the IR modules define those C names. - The libfuzzer and klee features are removed, with scripts/build-klee-runtime.sh and tests/klee_paths.sh; the post-processing self-tests move to scripts/test-klee-postprocess.sh. - map2check_assume* come from the glue IR (test-assume-link.sh); pending.txt is empty; rust-gap.tsv regenerated. - No --allow-multiple-definition or LEGACY exemption is left in the link tests. __m2c_rt_witness_enable is the C ABI of map2check_enable_witness. - tests/ffi_harness.c and test/*.c are rewritten against the C ABI and link the IR modules they need (scripts/build-c-abi-program.sh). - D5 artefacts removed (tests/core_api_coverage.rs, abi-mapping.tsv, symbol-matrix.sh). Version 2.0.0-rc.1; CHANGELOG, api-deltas, semantic-deltas, README and CLAUDE.md updated.
The removal of tests/klee_paths.sh (Task 2.10) took checks the drop-in core still needs: - build-test-runtime-bc.sh fails when the final Map2CheckFunctions.bc has 80 000 instruction lines or more, or llvm.bitreverse (--check-core, fixture test scripts/runtime-ir/test-core-checks.sh, CI); - test-klee-generator.sh runs a Rust panic in the core under KLEE (RUST_BACKTRACE=0 and full: the x == 7 path aborts in the panic code, no symbolizer frame, the other path completes) and the --wasm mode under symex (OVERFLOW at line 0, same files and ktests as the C). Also: SD-18 is `removed (2.0.0)` (no difference in the drop-in), SD-08 and SD-20 no longer point at deleted files, the map2check_success doc names __m2c_rt_witness_enable, the harness drops an unchecked claim and TODO.md no longer names the legacy KLEE route.
scripts/build-runtime-bc.sh <out-dir> (was the test build scripts/runtime-ir/build-test-runtime-bc.sh) writes exactly the 21 modules and refuses foreign files in <out-dir>; two clean builds give the same sha256 (scripts/test-build-runtime-bc.sh, which also runs the link matrix with and without --ref). scripts/it/overlay-install.sh copies a C install with cp -a and replaces only lib/*.bc (scripts/it/test-overlay-install.sh). The drop-in core now ends a run through the linked witness module, as Map2CheckFunctions.c:89-102: generate_aux_files(NULL, gotError), destroy, and on an error generate_confirmation_file and abort. Its generate_aux_files writes track_bb_log.st and calls the mode's analysis_generate_aux_witness_files and, on a violation or with MAP2CHECK_SEED_REPLAY, the generator's nondet_generate_aux_witness_files, the only writer of klee_log.csv. config.witness plays no part in the drop-in; __m2c_rt_witness_enable stays for the staticlib. Tests: scripts/runtime-ir/test-witness-wiring.sh (call count, files vs C with and without witness, klee_log.csv per generator, checked_error after wasm_rt_trap); the AFL++ crash replay through -witness-fuzzed.out now asserts map2check_checked_error; the KLEE test compares klee_log.csv and the witness files. CI: build/determinism on the host LLVM, overlay fixtures, and a runtime_matrix job that builds the image from develop.
User decision of 2026-10-27. With the KLEE generator's atomic writes on
(__m2c_rt_output_set_atomic(1)), a map2check_property whose content is not
a violation (NONE, UNKNOWN, empty) never replaces an existing one: it is
hard-linked from a complete temporary file, and link(2) fails with EEXIST
in one system call, so no other KLEE state can write between a check and
the replacement. A violation still replaces the target, as fopen("w").
Plain mode (AFL++, none) and the staticlib default are unchanged.
Fixes the KLEE unsafe-reach-none case, where a success state's NONE landed
after the violating state's TARGET-REACHED. SD-20 amended; the harness
exercises the switch in a forked scenario.
overlay-install.sh deleted an existing <out-install> whenever it had lib/Map2CheckFunctions.bc, which every C install has. The overlay now writes .map2check-overlay (source install, bc-dir, the 21 sha256) and removes only a directory with that marker; a C install given as output is refused and left untouched (new test). SD-20: a stale violation from an earlier KLEE run is kept against NONE; the frontend's fresh scratch directory (caller.cpp:94) makes it unreachable. CI runtime_matrix: show the fetched develop commit against the pinned one and warn when they differ, free disk space before the image build, and say that the job has not run on a runner yet.
The frontend compiles the program linked with Map2CheckFunctions.bc three times with afl-clang-fast (fuzzed, witness, cmplog), and that time grows with the core's IR. The pre-gate timing (Task 4.1a) put rust/C at 2.78 (afl 9.31, hybrid 7.25, symex 1.21). - rust/src/cfmt.rs: the %u, %d, %p, %lf and %.9g of glibc into a byte buffer, exact (tested against glibc's snprintf on 12 000 values), so the result files no longer go through core::fmt and its float code. - rust/src/sys.rs: the libc calls std::fs, std::env and std::process made (open64, write, close, rename, linkat, unlink, getpid, getenv, __xpg_strerror_r), with the same flags and the same error texts. - Map2CheckError formats its own messages; thiserror is gone. - The drop-in build has no serde/serde_json (no JSON channel), no catch_unwind (panic = abort), no old-API leak checks, no OnceLock, and is built at opt-level z. klee/Cargo.toml has no dependencies. - write_property builds its text once; the byte appends are not inlined. - build-runtime-bc.sh fails above 9 500 instruction lines or 13 600 IR lines (the values reached plus about 7%). Core: 34 582 -> 8 865 instruction lines, 43 340 -> 12 741 IR lines, 762 580 -> 327 164 bytes; one afl-clang-fast -g -O2 of the smoke program 1.74 s -> 0.60 s. Files, diagnostics and the C ABI are unchanged.
write_property took the #[repr(C)] ViolatedProperty enum by value, so a C caller passing an int outside 0..=10 was undefined behaviour before ffi_guard ran. It now takes the C int (ViolatedPropertyRaw) and maps it with violated_property_from_raw; a value with no enumerator leaves map2check_property empty, as the C switch does. cbindgen excludes the alias and renames it, so the header keeps `enum ViolatedProperty` (the enum is exported explicitly, since write_property no longer pulls it in). c_str mapped a C string that is not valid UTF-8 to "", so a violation wrote `Function: ` with no name where develop prints the bytes with %s. It now converts lossily: valid UTF-8 is borrowed unchanged, an invalid sequence becomes U+FFFD. Also fix the stale "ONLY module with unsafe code" comment of ffi.rs: sys.rs and wasm.rs have unsafe blocks too. Final review, minor items 1, 2 and 6.
- Copy $CHANGELOG_FILE, the file the script checks, instead of the root CHANGELOG.md. - cargo build --locked. - Remap the repository and the cargo registry/git paths with --remap-path-prefix (own target directory, target/package-release), so the staticlibs no longer embed the builder's home directory; the package test checks both libraries with strings and that the packaged CHANGELOG is CHANGELOG_FILE. Final review, minor item 5.
…iles - integration-guide.md, Call order: a program linked by hand with the staticlib calls analysis_init() and nondet_init() of the linked modules after map2check_init; without them the mode stays unset. - handoff-map2check.md: the gates ran no overflow task, no coverage-* property and no --btree/--wasm run, and where those are covered instead. - semantic-deltas.md, SD-20: a KLEE state killed between creating its temporary file and the rename can leave a .tmp file behind. Final review, minor items 3, 7 and 8.
…ename llvm-as-16 records the input path as source_filename. On a host with the LLVM 16 tools (CI) the work directory differs per build, so two clean builds of the 20 IR modules differed and the determinism test failed. Assemble from inside ll/ so the name is <module>.ll.
tests/gate_deltas.rs runs scripts/runtime-ir/gen_ll.py to check the generated KLEE main (SD-24); the test stage had neither, so the coverage run failed in CI.
feat!: drop-in Rust runtime for Map2Check develop (2.0.0-rc.1)
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 2.0.0-rc.1 (docs/release.md, passo 4). Inclui o runtime drop-in do Map2Check develop (#56): ABI C do runtime (D6), os 21 módulos .bc (D7), empacotamento e os dois gates diferenciais (docs/cutover/gate-2026-10-27.md, docs/cutover/gate-2026-10-28.md). Tag assinada v2.0.0-rc.1 e prerelease já publicadas sobre o commit 8b9d367 de develop.