README.md

---
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:

```sh
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

```sh
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:

```sh
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](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](https://huggingface.co/docs/hub/spaces-sdks-docker#secrets-and-variables-management)
and [downloadable Space images](https://huggingface.co/docs/hub/spaces-run-with-docker).

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.