Spaces:
Sleeping
Sleeping
| 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. | |