Prepare the library to replace the Map2Check C runtime (1.1.0-rc1)

.github/workflows/CI.yml

@@ -33,6 +33,16 @@ jobs:
       - name: Rodar todos os testes
         run: cargo test --all-features
 
+      # O espelho de wasm_rt_memory_t / wasm_rt_funcref_table_t (feature wasm)
+      # só é conferido contra o wasm-rt.h do wabt quando WASM_RT_INCLUDE existe.
+      - name: Conferir o layout de wasm-rt.h (wabt 1.0.41)
+        run: |
+          mkdir -p target/wabt-include
+          curl -fsSL https://raw.githubusercontent.com/WebAssembly/wabt/1.0.41/wasm2c/wasm-rt.h \
+            -o target/wabt-include/wasm-rt.h
+          WASM_RT_INCLUDE="$PWD/target/wabt-include" \
+            cargo test --features wasm --lib layout_matches_wasm_rt_h
+
       - name: Testar script de proteção de branches
         run: scripts/test-branch-protection.sh
 
@@ -84,6 +94,25 @@ jobs:
           done
           [ "$ok" = 1 ]
 
+      # The harness rejects inputs with __VERIFIER_assume(0), which unwinds
+      # through the C frame of its __map2check_main__ (D1 condition 11).
+      # Optimised builds are where a missing unwind path would show: once
+      # with -fexceptions, the flag the pipeline must use, and once with
+      # clang's defaults.
+      - name: Compilar e executar harness FFI em -O2 (com e sem -fexceptions)
+        run: |
+          cargo build --release --all-features
+          for flags in "-fexceptions" ""; do
+            clang -O2 $flags -fsanitize=address,undefined -fno-omit-frame-pointer \
+              tests/ffi_harness.c target/release/libmap2check.a \
+              -ldl -lpthread -lm -o target/ffi_harness_o2
+            ok=0
+            for i in 1 2 3 4 5; do
+              if target/ffi_harness_o2; then ok=1; break; fi
+            done
+            [ "$ok" = 1 ] || { echo "ffi_harness -O2 $flags falhou"; exit 1; }
+          done
+
       - name: Compilar e executar test/codeAPI_by_caller_test.c (API núcleo)
         run: |
           cargo build --release
@@ -137,4 +166,55 @@ jobs:
         run: cargo audit
 
       - name: Build do Dockerfile
-        run: docker build .
+        run: docker build .
+  # Runtime do gerador `symex` (D1, rota A′; docs/klee-feasibility.md): as
+  # mesmas fontes compiladas por rustc 1.72.1 (LLVM 16) a partir de
+  # klee/Cargo.toml e do seu Cargo.lock v3, em bitcode que o llvm-link-16 e o
+  # KLEE 3.1 leem. O clippy em 1.82 do job acima não vê o que o 1.72 não
+  # compila (`LazyLock`, `unsafe extern`, API de std posterior a 1.72): este
+  # job é a guarda da condição 5. O KLEE em si não roda aqui (a imagem com o
+  # KLEE 3.1 é a do Map2Check); tests/klee_paths.sh roda no CI do Map2Check
+  # (Task 3.4) e localmente com Docker.
+  klee_runtime:
+    runs-on: ubuntu-24.04
+    steps:
+      - name: Baixar o código do repositório
+        uses: actions/checkout@v4
+
+      - name: Instalar as ferramentas do LLVM 16 (opt, llvm-dis, llvm-nm, llvm-as, lli)
+        run: sudo apt-get update && sudo apt-get install -y llvm-16
+
+      - name: Instalar o rustc 1.72.1 (LLVM 16) com clippy
+        run: rustup toolchain install 1.72.1 --profile minimal --component clippy
+
+      # O clippy em 1.82 do job acima não compila nondet/klee.rs (feature
+      # `klee` só existe em klee/Cargo.toml); este é o lint dele.
+      - name: Clippy do build KLEE (rustc 1.72.1, feature klee)
+        run: RUSTUP_TOOLCHAIN=1.72.1 cargo clippy --locked --manifest-path klee/Cargo.toml --features klee,wasm -- -D warnings
+
+      # O script roda os autotestes da troca de intrínsecos antes de usá-la:
+      # equivalência por lli-16 em tests/klee/lower-intrinsics.ll e recusa
+      # de tests/klee/unknown-intrinsic.ll; qualquer intrínseco que o KLEE
+      # 3.1 não execute faz o build falhar. Antes da troca, o simbolizador
+      # de backtrace do std vira stubs de abort (scripts/klee-stub-symbolizer.py,
+      # com autoteste em tests/klee/stub-symbolizer.ll), e a guarda final
+      # falha se algum corpo do simbolizador sobrar.
+      - name: Compilar o runtime KLEE em bitcode (klee/Cargo.toml, --locked)
+        run: scripts/build-klee-runtime.sh target/klee/map2check-klee.bc
+
+      - name: Verificar que o bitcode existe e é legível pelo llvm-dis-16
+        run: |
+          test -s target/klee/map2check-klee.bc
+          llvm-dis-16 target/klee/map2check-klee.bc -o /dev/null
+
+      - name: Checar dependências do lockfile KLEE (cargo-deny)
+        uses: EmbarkStudios/cargo-deny-action@v2
+        with:
+          manifest-path: ./klee/Cargo.toml
+
+      - name: Publicar o bitcode do runtime KLEE
+        uses: actions/upload-artifact@v4
+        with:
+          name: map2check-klee-bc
+          path: target/klee/map2check-klee.bc
+          if-no-files-found: error

CHANGELOG.md

@@ -15,15 +15,80 @@ the C ABI or the JSON report must update them.
 
 ## [Unreleased]
 
+## [1.1.0-rc1] - Unreleased
+
+Release candidate of the cutover work: the library becomes the runtime of
+Map2Check (Tasks 1.2, 2.1-2.5, 2.7 and 2.8 of the cutover plan). Read the
+breaking changes first.
+
+### Breaking changes
+
+- `map2check_check_free` and `map2check_map_free` take one more argument, the
+  address of the pointer variable (the pointer slot), so the free is logged
+  like the C runtime does. Passes built against 1.0.0-rc1 must be rebuilt
+  (`docs/api-deltas.md`).
+- `map2check_set_mode` takes an `int32_t`. Invalid modes are rejected.
+- Default verdicts changed: the end-of-program leak check (memcleanup) is no
+  longer opt-in, and the first violation is final; a later passing check does
+  not clear it (#36). See `docs/semantic-deltas.md`.
+- With an analysis mode set, the library prints no JSON, and an unreadable
+  fuzzer input ends the run instead of continuing.
+
 ### Added
 
+- Runtime profile `runtime` (`cargo build --profile runtime --features
+  libfuzzer,wasm`): release optimisations with `panic = "unwind"`, so the FFI
+  guard can recover panics. This is the build Map2Check links.
+- Lifecycle: `map2check_init` and every fuzzer iteration reset the analysis
+  state (#9); every export is guarded against panics and works before
+  `map2check_init` (#8).
+- Runtime analysis modes: `map2check_set_mode` and `map2check_reach_target`
+  select assert, overflow, memory or reachability checking at run time.
+- Legacy result files consumed by Map2Check (property, log and witness files)
+  and abort on the first violation (#19, #14).
+- Core API completion: signed binary operations checked at the operation's
+  width with `DivByZero`, `posix_memalign` tracking through the `void **` it
+  wrote (#13), the full `__VERIFIER_nondet_*` family logged as develop writes
+  it (#6), AFL++-style fuzzer input reading, and rejection of
+  `__VERIFIER_assume` inside loops.
+- KLEE runtime (#20): `klee/Cargo.toml`, a second manifest built with rustc
+  1.72.1 (LLVM 16) into one bitcode module by
+  `scripts/build-klee-runtime.sh`, with CI. The bitcode is built separately
+  and is not in the release archive.
+- The KLEE bitcode now includes the `wasm` feature (`--features klee,wasm`): the `wasm_rt_*` stubs and the `map2check_wasm_*` exports, so Map2Check's `--wasm` mode with the `symex` generator no longer stops with "failed external call: wasm_rt_is_initialized". `tests/klee_paths.sh` runs a wasm2c-lifted module (`tests/klee/wasm.c`) and expects OVERFLOW at line 0, as develop's C runtime gives (SD-19).
+- `lib/libmap2check_runtime.a` in the release archive: the `runtime` profile
+  with features `libfuzzer,wasm`.
+
+- Feature `wasm`: the runtime of Map2Check's `--wasm` mode (D2) ported from the
+  C runtime: the `wasm_rt_*` stubs, `w2c_wasi__snapshot__preview1_proc_exit` and
+  `map2check_wasm_malloc`, `map2check_wasm_free`, `map2check_wasm_check_access`
+  (SD-19). `tests/core_api_coverage.rs` checks every `core_symbol` of
+  `docs/cutover/abi-mapping.tsv` against the staticlib.
 - `docs/api-deltas.md` symbol/signature matrix for the core C API and the
   Map2Check passes, and `docs/semantic-deltas.md` with reproducible
   behaviour differences, both checked by `tests/compat_docs.rs` (#5).
 - `docs/integration-guide.md` and `docs/release.md`;
   `scripts/package-release.sh` builds the release archive with the C
   header, both static libraries and the docs (#5).
 
+### Fixed
+
+- Memory tracking: addresses are validated by their latest alloc/free event
+  (#11), an untracked resolved free is reported as invalid (#37), a passing
+  resolved free records the release (#11, #37), and a VLA is a static slot
+  sized in elements (#38).
+- Option semantics: `memcleanup` and null-is-valid are honoured by the memory
+  checks, and runtime options are separate from the analysis configuration
+  (#10).
+- The memcleanup verdict matches develop's.
+- Throughput of the KLEE (`symex`) runtime: the load check no longer builds a
+  hash set per call, the check context borrows the function name, and no
+  build is instrumented for coverage any more (the repo-wide
+  `.cargo/config.toml` that added `-C instrument-coverage` is removed;
+  `cargo tarpaulin` adds it itself, and `scripts/build-klee-runtime.sh`
+  rejects it). On list-ext the runtime spends about 4 times fewer KLEE
+  instructions per path and finds the FALSE-DEREF that it missed before.
+
 ### Changed
 
 - `develop` replaces `feature/rust` as the integration branch: CI runs on