README.md

metadata

title: Decompiler verifier
emoji: 🔍
colorFrom: indigo
colorTo: blue
sdk: docker
app_port: 7860
fullWidth: true

Decompiler verifier workbench

Public Gradio frontend for comparing a binary function with candidate C. Select an example or upload an ELF x86-64 binary, supply its function address and candidate source, and stream verification results with assembly previews and a JSON download. The application includes 63 examples in expandable sections: Basics, Calls and memory, Types and ABI, Real binaries, Related work, and Ghidra exports. Each section has a short description with relevant paper or tool links. Basics starts open; expand any other section to browse its examples. Example labels show the expected result with the bundled settings: green for agreement, yellow for inconclusive results or compilation/type errors, and red for mismatches.

The verification library is a private GitHub repository referenced by the core/ Git submodule. This repository publishes the UI and demo assets. Running verification locally requires access to the private core; cloning the public frontend alone does not grant that access.

Local development

Use Linux/amd64, Python 3.11.13, GCC, Clang 18, and binutils. On macOS or Windows, use the Docker workflow below. With authorized GitHub credentials:

git submodule update --init --checkout core
uv sync --locked
bash core/native/build.sh build/decompile-verify-declarations
export PATH="$PWD/build:$PATH"
uv run python -m demo.app
uv run python -m pytest -q

Open http://localhost:7860. The library is installed as an editable dependency from the submodule. Building the helper outside Docker requires llvm-18-dev, libclang-18-dev, and libclang-cpp18-dev; Docker installs them in a cached toolchain layer. UI tests operate on public assets and the installed library; they do not import the private engine tests. Core regression tests run separately in the core project.

Memory mismatches show the last writer of the differing byte in each execution: the instruction address, assembly, and store address and size. A side that never wrote the byte is marked as initial memory. These details appear in both the first mismatch summary and downloaded JSON (original_writer and candidate_writer). Candidate writer lines are highlighted in the C editor using compiler debug-line information. The writing instructions are highlighted in both assembly panes, even without C source mapping. Highlights clear when inputs become stale; -g0 disables source mapping. Return-value mismatches also highlight their producing instructions and candidate C lines. original_writers and candidate_writers in the JSON report identify the last writes covering the differing bytes of the return value or aggregate field. Several instructions can contribute to one return, including partial register writes. Call mismatches highlight the actual call or tail-jump instruction on each present side and its candidate C lines. Argument mismatches also show and highlight the last writers of the differing argument bytes, including stack arguments, aggregate fields, and explicit pointer byte ranges. JSON reports include original_callsite, candidate_callsite, and argument original_writers / candidate_writers. An extra or missing call highlights the first unpaired call on the side containing it. The writers identify the operations that produced the observed bytes; the cause of an incorrect value or destination may be an earlier calculation.

Docker and Hugging Face

docker build --platform linux/amd64 -t decompile-verify:gradio .
docker run --rm --platform linux/amd64 --publish 127.0.0.1:7860:7860 \
  --env CORE_GITHUB_TOKEN decompile-verify:gradio

Set CORE_GITHUB_TOKEN in your local environment using your credential manager before running the command; do not write its value into shell history. In the Space Settings, configure the same name as a secret. Use a GitHub token scoped to the private core repository with read-only Contents permission.

The public image contains third-party dependencies and UI code. It excludes the private submodule even when initialized locally. At startup, bootstrap.py fetches the pinned core commit, verifies it, installs the library, builds its native Clang helper, retains the checkout without Git metadata, removes the token from the application environment, and launches Gradio on port 7860. Startup fails clearly if credentials or the pinned revision are unavailable. This requires network access to GitHub at startup. The core checkout, installed library, and helper exist only in the running container, outside the published image. The image includes the public LLVM development toolchain so startup can build the helper without putting private source or executables in image layers. uv uses a BuildKit cache mount for dependency downloads and builds; that cache is reused across builds and does not become part of the published image.

Uploads and downloaded reports are ephemeral. Gradio blocks file serving from the private library, native helper, development submodule, and Git metadata. The workbench preserves queued streaming, cancellation, editable settings, and deterministic JSON reports.

Update the core revision

Commit and push library changes in the private core repository first. Update the submodule to that committed revision, then regenerate pin metadata and dependencies:

git -C core fetch origin
git -C core checkout CORE_COMMIT
uv run --no-sync python scripts/pin_core.py

Commit core, core-revision.json, uv.lock, and requirements-runtime.txt together. The private core stays on GitHub; only its gitlink is published here. The Docker build installs the hashed requirements without authenticating to GitHub. The submodule uses update = none to prevent hosting builders from attempting to clone private code before the Docker build. Local developers use the explicit --checkout option above; runtime startup fetches the recorded commit separately.

Startup retains the pinned private core checkout in core/ after removing its Git metadata. The UI reads example sources from that checkout and compiles originals when preparing examples. Local development uses the same loader and submodule. The Related work section combines nine Faultless cases with nine cases from D-Helix, DiscScope, and Decompile-Diverge, including a deliberately uncompilable export. See core/docs/related-work-examples.md for provenance, interface adaptations, and published counterexamples. The three O0 completeness pairs (my_putchar_count, upper, and print_page_header) are stored in demo/cases/, including raw exports, source metadata, and documented runnable adaptations in demo/cases/README.md. Reference C is a display aid; uploaded binaries have none. DiscScope orig.c excerpts are stored alongside their raw.c and cand.c in the shared core cases. They come from binutils 2.29, libsmi 0.4.8, and JasPer 1.900.16, with source locations, checksums, and license notices. Verification uses the published DiscScope binaries. The bundled factor executable and redistribution notices are read from core/examples/binaries/ and copied together into the prepared example directory.

Publish under the existing Space name

The old private ejschwartz/decompile-verify Space contains core source and history. Do not make it public directly. Back it up privately, then create a clean replacement at the same name and push only this repository's fresh history. Configure secrets, validate the app and all image layers while private, and verify old core-containing commits and images are inaccessible before publishing. Replacing the Space requires separate approval because it interrupts the current app and removes its history/settings.

See Docker Space secrets and downloadable Space images.

To inspect every image layer for private core files and repository metadata, run python scripts/audit_image.py decompile-verify:gradio. The audit recognizes uv's empty cache sentinel as installer metadata rather than a project Git repository.

Execution modes and replay

Number of executions counts shared-input comparisons: one input tested against both functions. The initial seed controls reproducibility. Core Python/YAML tasks use execution_count; seed_count remains a deprecated alias. Reports from the execution-budget interface use verifier-report-v4 and include saved recipes.

concolic collects symbolic branch conditions during the same function runs used for comparison. It solves alternative branches and queues generated testcases. When the queue has inputs, Fresh random input probability chooses between a new random input and the oldest generated input; the default is 25% random. An empty queue always selects random. The execution table’s Source column shows how each input was chosen: random sampling, concolic solving, comparison guidance, or replay. Max new testcases per run caps children generated across both sides of one comparison (default 8), and Solver timeout per query bounds each solver request (default 1000 ms). All three settings are configurable.

Concolic inputs include integer/pointer argument leaves, lazy memory bytes, and intercepted call responses. Address and indirect-target expressions are restricted to observed concrete values and reported. Floating-point solving and pointer topology exploration are deferred. Reports record testcase lineage, solver outcomes, tracking limitations, and whether the intended branch was reached. Agreement describes the tested inputs, not universal equivalence.

The frontend defaults to comparison_guided, including API calls that omit the mode. Run settings show options for the selected execution mode. random has one NULL probability, applied equally to arguments, lazy memory words, and call responses (zero for non-pointer values). Other values are sampled randomly. comparison_guided starts with uniform random inputs and exposes the repeated branch threshold and learned-value probability. The threshold counts consecutive identical outcomes at the same branch before learning. Once relevant values are learned, the probability controls how often to choose them instead of random values. Inactive settings do not affect the run.

Guidance only changes new input assignments; both functions are compared on a frozen shared recipe. Discovery instruction and branch-observation counts appear separately.

Alternate-mode JSON reports include replay recipes. Upload a standalone recipe or a downloaded report in Replay recipe or report (JSON) to replay one fixed input; a report selects its first recipe. Replay retains the worker-process cancellation behavior and checks that the binary, candidate, interfaces, and compiler settings match. See core/docs/execution-modes.md for the design and core Python API.