Map2Check is a bug hunting tool that automatically generates and checks safety properties in C programs and WebAssembly (WASM) binaries. It tracks memory pointers and variable assignments to check user-specified assertions, overflow, and pointer safety. The generation of the test cases is based on assertions (safety properties) from the code instructions, adopting the LLVM framework version 16, AFL++, KLEE to generate input values to the test cases generated by Map2Check.
WASM verification works by lifting .wasm binaries to LLVM IR (via WABT's wasm2c + clang-16) and reusing the existing Map2Check instrumentation passes and the KLEE backend — see Verifying WebAssembly (WASM) binaries.
Extra documentation is available at https://map2check.github.io
A video explaining Map2Check is available on YouTube:
To use the Map2Check tool is necessary a Linux 64-bit OS system (Ubuntu 22.04 recommended). In the linux OS, you should install the requirements, typing the commands:
$ sudo apt install python3 libc6-devOur binary tool is avaliable at https://github.com/hbgit/Map2Check/releases
In order to install Map2Check on your PC, you should download and save the map2check zip file on your disk from https://github.com/hbgit/Map2Check/releases. After that, you should type the following command:
$ unzip map2check-vx.y.2026-ii.jj.140ba2d2.zip
$ cd map2check-vx.y.2026-ii.jj.140ba2d2Releases starting from v8.0.0-Songbirds include WebAssembly verification support (the --wasm option and the lib/WasmRuntimeStubs.bc runtime). Note that verifying .wasm inputs additionally requires WABT 1.0.41 and clang-16 installed on the host — see Verifying WebAssembly (WASM) binaries. To generate a release layout yourself, build inside the Docker image and run ninja install: the self-contained distribution (binary, KLEE, instrumentation bitcode and WASM runtime) is produced in the release/ directory.
Map2Check can be invoked through a standard command-line interface. Map2Check should be called in the installation directory as follows:
Example programs are available in the examples/ directory.
$ ./map2check --memtrack program.cIn this case, --memtrack is the option to check for memory errors. For help and others tool options:
$ ./map2check --helpWhen you use a LLVM bytecode as input for the tool, be sure to add -g flag when generating the file, it is not required, but map2check will provide better info (like line numbers).
Map2Check generates inputs with two engines: the AFL++ 4.40c fuzzer (persistent mode, PCGUARD,
CmpLog) and the KLEE 3.1 symbolic executor. By default, and whenever --timeout is
given, the two run as an alternating hybrid. They take turns, each turn ends once its engine stops
finding new coverage, and every round doubles the turn's window. The engines also hand each other
input vectors.
| Option | Effect |
|---|---|
(default, with --timeout) |
Alternating hybrid with seed exchange. Same as --alternate-engines. |
--fixed-hybrid |
The 8.x schedule: the fuzzer for 0.2 of the budget, then KLEE. |
--fixed-hybrid --seed-exchange |
The 8.x schedule with seed exchange (0.2 / 0.6 / 0.2, with a last fuzzer phase). |
--nondet-generator afl / symex |
One engine only: AFL++ or KLEE. In 8.x the fuzzer value was fuzzer. |
--slice |
Slice the program before the analysis (sbt-slicer), for reachability, --check-asserts, --memtrack, --memcleanup-property and --check-overflow. |
--generate-test-suite |
Emit a Test-Comp test suite (test-suite/). |
--generate-test-suite --cover-branches |
Emit a Cover-Branches suite, up to 50 cases, from KLEE's paths and the fuzzer's corpus. |
--add-invariants |
Optional, and off in the default build. See below. |
Verdicts. A TRUE verdict needs KLEE to have explored every path. Map2Check reports
UNKNOWN instead when KLEE stopped early for any reason:
- its timer ran out;
- it concretized a symbolic input (for example a floating-point value);
- it killed states;
- it hit its memory cap;
- it crashed.
A call to abort() in the program under analysis is treated the way SV-COMP treats it: as
an assumption. It prunes that path and does not end the search.
Environment knobs. These exist for experiments; the defaults are the measured choices.
| Variable | Default | Meaning |
|---|---|---|
MAP2CHECK_FUZZER_SUITE |
on | 0 leaves the fuzzer's corpus out of Cover-Branches suites. |
MAP2CHECK_SLICE_CLEANUP |
none | light or o2: an opt pipeline over the fresh slice. Measured neutral. |
MAP2CHECK_SLICER_FLAGS |
— | Extra sbt-slicer flags, e.g. --cda=ntscd. Measured neutral. |
MAP2CHECK_PREOPT |
off | ssa: mem2reg + simplifycfg before instrumentation, for reachability and assert only. Measured neutral in the hybrid. |
MAP2CHECK_CHECK_CSTRINGS |
off | 1: check the strings a %s or puts reads. It fixes one wrong TRUE on Juliet, but produces false positives on memory the runtime does not track (CASTLE: FP from 1 to 4). |
MAP2CHECK_CLAM_PROFILE |
default | memory or none: see --add-invariants. |
MAP2CHECK_KLEE_MAX_MEMORY |
KLEE's 2000 | KLEE's --max-memory, in MB. Raising it to 6000 changed nothing on Intel-TDX (0/8 either way). |
--add-invariants inserts abstract-interpretation invariants computed by
Clam (formerly crab-llvm). The build must be configured
with -DENABLE_CLAM=ON and Clam installed at $CLAM_DIR; otherwise the option is
refused with exit code 3.
The option stays optional while it is under study. So far:
- In the SV-COMP 2019/2020 builds, the invariants reached neither the instrumentation nor KLEE: they were emitted as
llvm.assume. - On the current hybrid, the first measurement found no gain.
- Clam is bounded to 0.2 of the budget and falls back to the plain compile when it fails.
- A dedicated study round is planned. See
docs/reports/tacas-experiment-log.md(INV-1, R25).
Measurements of every option above are recorded in docs/reports/tacas-experiment-log.md.
Map2Check can verify third-party .wasm binaries (e.g. IoT/Edge modules) without access to their source code. Instead of implementing a dedicated WASM verification engine, Map2Check lifts the binary to LLVM IR and reuses its consolidated instrumentation passes and SMT-based backend:
.wasm ──▶ [1] Lifter: wasm2c (WABT) → C → clang-16 → LLVM IR
──▶ [2] Map2Check passes (WASM mode): linear-memory bounds checking,
overflow and reachability instrumentation
──▶ [3] KLEE symbolic execution
──▶ [4] Result: TRUE / FALSE / UNKNOWN + witness
The analysis is language-agnostic: it instruments the elements common to every lifted module (the linear memory array and the wasm_rt_* runtime calls), so it works regardless of whether the .wasm was produced from C, Rust, Go, or AssemblyScript. Properties currently detected on WASM inputs:
| Property | Example CWEs | Status |
|---|---|---|
| Linear-memory out-of-bounds access (bounds checking) | CWE-121/122/124/126/127 | ✅ Supported |
| Arithmetic overflow | CWE-190 | ✅ Supported |
| Reachability of target/error functions | — | ✅ Supported |
| Memory leak / use-after-free / double-free | CWE-401/416/415 | ❌ Future work¹ |
¹ In lifted WASM code the source language's allocator is compiled inside the linear memory, so malloc/free calls are not visible in the IR. Full memory tracking requires an export convention or allocator-detection heuristics — planned as future work.
- WABT ≥ 1.0.41 —
wasm2conPATHand thewasm-rt.hheaders (searched at/opt/wabt-1.0.41/include, then/opt/wabt/include, then/usr/include). Thewabtpackage from Ubuntu apt (1.0.27) is too old; install the GitHub release. - clang-16 at
/usr/bin/clang-16(used to compile the lifted C to LLVM bitcode).
Both are pre-installed in the development Docker image (Dockerfile.dev). Only .wasm (binary) files are accepted; for a .wat (text format) file, convert it first with wat2wasm module.wat -o module.wasm (also part of WABT).
$ ./map2check --wasm --memtrack --timeout 290 module.wasmRelevant options:
--wasm— enable the WASM pipeline (lifting + WASM-mode instrumentation). Implies memtrack mode.--entry-function <name>— override the entry function name (default:main). Map2Check automatically generates amain()wrapper that initializes the wasm2c runtime and calls the module'sw2c_*_startentry point, so in most cases you do not need this flag.--timeout <s>— give KLEE enough time to explore the lifted IR. Lifted modules embed the whole WASI libc, so short timeouts (e.g. 110 s) tend to yieldUNKNOWN; 290 s is the value validated on the Juliet benchmarks.
Inside the development container, create a C program with a heap buffer overflow, compile it to WASM with the wasi-sdk (pre-installed at $WASI_SDK_PATH), and verify the resulting binary:
$ cat > test_heap_overflow.c << 'EOF'
#include <stdlib.h>
int main() {
int* p = (int*)malloc(10 * sizeof(int));
if (!p) return -1;
p[0] = 42;
p[10] = 999; /* out-of-bounds write */
free(p);
return 0;
}
EOF
$ $WASI_SDK_PATH/bin/clang --target=wasm32-wasip1 \
test_heap_overflow.c -o test_heap_overflow.wasm
$ ./map2check --wasm --memtrack --timeout 290 test_heap_overflow.wasm
# Expected result:
Adopting z3 solver...
Started Map2Check
WASM mode: lifting test_heap_overflow.wasm
...
----------------------------------------------------
Violated property:
file map2check_property line 8 function main
OVERFLOW
VERIFICATION FAILEDA safe program (e.g. writing to p[9] instead of p[10]) is not flagged. The pipeline was validated on a subset of the Juliet Test Suite compiled to WASM (CWE-121/122/124/126/127): all 15 seeded bugs were detected as FALSE with a 290 s timeout — see docs/reports/wasm-juliet-validation.csv. The integration test scripts tests/integration/test_wasm_pipeline.sh and tests/integration/test_wasm_entrypoint.sh reproduce this workflow automatically.
You can build Map2Check using our development Docker image (Dockerfile.dev), which provides Ubuntu 22.04 with LLVM 16, KLEE 3.1, WABT 1.0.41 and wasi-sdk 33.0 pre-installed:
$ git clone https://github.com/hbgit/Map2Check.git
$ cd Map2Check
# Build the development Docker image
$ docker build -t map2check-dev --no-cache -f Dockerfile.dev .
$ docker run -it --rm -v $(pwd):/workspace map2check-dev /bin/bashInside the container:
$ mkdir build && cd build
$ cmake .. -G Ninja \
-DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm
$ ninja && ninja install
# binário em: release/bin/map2check (ou release/map2check)The Dockerfile.dev image already builds and installs KLEE 3.1 (to /opt/klee) and installs AFL++ 4.40c as a standalone toolchain (found at run time under /usr/local/bin), so do not pass -DSKIP_KLEE=ON or -DSKIP_AFL_PLUS_PLUS=ON — those flags skip the cmake/FindKlee.cmake / cmake/FindAFLPlusPlus.cmake modules entirely. Only pass them ON if you deliberately want a build without KLEE/AFL++ support (e.g. -DSKIP_AFL_PLUS_PLUS=ON -DSKIP_KLEE=ON for a minimal/CI build).
Building with WASM support requires no additional CMake flag — the WasmLifter frontend module is always compiled. The only extra build-time dependency is the WABT 1.0.41 header wasm-rt.h: when CMake finds it (searched at /opt/wabt-1.0.41/include, /usr/include, /usr/local/include), it compiles the KLEE-compatible wasm2c runtime WasmRuntimeStubs.c to bitcode and installs it as release/lib/WasmRuntimeStubs.bc, which is linked into the lifted module when --wasm is used. If wasm-rt.h is not found, CMake prints a warning and the build proceeds without WASM support (the recommended way to get a WASM-enabled build is the Docker image above, which ships WABT and the wasi-sdk out of the box).
Minor test:
$ cd ../release/
$ ./map2check --memtrack svcomp_960521-1_false-valid-free.c
# Expected Result:
Adopting z3 solver...
Started Map2Check
Compiling /workspace/release/../tests/regression_test/test_cases/sv-benchmarks/memsafety/960521-1-1.c
...
>>Memory list log
Line content : { free(a); free(b); } /* ditto */
Address : 0x55ba60a90700
PointsTo : 0x7f95f0003d54
Is Free : TRUE
Is Dynamic : FALSE
Var Name : b
Line Number : 29
Function Scope : main
----------------------------------------------------
Violated property:
file map2check_property line 29 function main
FALSE-FREE: Operand of free must have zero pointer offset
VERIFICATION FAILEDRequires: CMake ≥ 3.20, C++17, LLVM 16, Boost.
More details at https://map2check.github.io/docker.html
Unit tests (no KLEE/AFL++ required):
$ mkdir build && cd build
$ cmake .. -G Ninja \
-DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \
-DSKIP_AFL_PLUS_PLUS=ON -DSKIP_KLEE=ON -DENABLE_TEST=ON
$ ninja && ctest --output-on-failure
# Expected results:
Test project /workspace/build
Start 1: HelloGTest
1/7 Test #1: HelloGTest ....................... Passed 0.00 sec
Start 2: AllocationLogTest
2/7 Test #2: AllocationLogTest ................ Passed 0.00 sec
Start 3: HeapLogTest
3/7 Test #3: HeapLogTest ...................... Passed 0.00 sec
Start 4: ContainerReallocTest
4/7 Test #4: ContainerReallocTest ............. Passed 0.00 sec
Start 5: BTreeTest
5/7 Test #5: BTreeTest ........................ Passed 0.06 sec
Start 6: ContainerBTreeTest
6/7 Test #6: ContainerBTreeTest ............... Passed 0.05 sec
Start 7: MemTrackTest
7/7 Test #7: MemTrackTest ..................... Passed 0.00 sec
100% tests passed, 0 tests failed out of 7WASM integration tests (require the Docker image, i.e. KLEE + WABT + wasi-sdk):
$ ./tests/integration/test_wasm_pipeline.sh # heap overflow detection + CLI flag
$ ./tests/integration/test_wasm_entrypoint.sh # entry-point wrapper generationThese are also run on every push/PR by the e2e-wasm job in .github/workflows/ci.yml, which exercises the full .wasm → LLVM IR → passes → KLEE pipeline inside the published map2check-dev image.
Use the map2check-wrapper.py script in the Map2Check binary directory to verify each single test-case.
Usage:
$ ./map2check-wrapper.py -p propertyFile.prp file.iMap2Check accepts the property file and the verification task and provides as verification result: TRUE + Witness, [FALSE|FALSE(p)] + Witness, or UNKNOWN. FALSE(p), with p in {valid-free, valid-deref, valid-memtrack, valid-memcleanup}, means that the (partial) property p is violated. For each verification result the witness file (called witness.graphml) is generated Map2Check root-path folder. There is timeout of 897 seconds set by this script, using "timeout" tool that is part of coreutils on debian. If these constraints are violated, it should be treated as UNKNOWN result.
Maintainers:
- Herbert O. Rocha (since 2014), Federal University of Roraima, Brazil - https://hbgit.github.io/
- Rafael Menezes (since 2016), Federal University of Roraima, Brazil - https://rafaelsa94.github.io/
- Guilherme Bernardo (since 2025), Federal University of Roraima, Brazil - https://github.com/GuilhermeBn198
Questions and bug reports:
E-mail: map2check.tool@gmail.com
.-.
/v\
// \\ > L I N U X - GPL <
/( )\
^^-^^
bug found -> verified safe
Map2Check . Linux . GPL