Faultless: A Program Equivalence Technique for Validating and Evaluating Neural Decompilers

1 Introduction

• Neural decompilers can restore names, types, and structured control flow, but semantic mispredictions can incorrectly represent program functionality.Compilation discards source-level features, leaving traditional decompilers with code that can be difficult for reverse engineers to understand.Source: §1 · p. 1
• Faultless detects semantic mispredictions by comparing neural output with deterministic decompilation for validation, or with the original code for evaluation.Deterministic decompilers produce less readable output but have stronger correctness properties.Source: §1 · pp. 1–3
• Equivalence checking must handle functions without most dependency information, which prevents typical compilation and makes many existing checking techniques unusable.Faultless relies on type definitions, which prior type-prediction work and LLMs may provide.Source: §1 · p. 3
• Validation must tolerate systematic semantic differences between deterministic and ideal neural decompilations, so Faultless abstracts away compiler-specific details where possible.Optimizations can restructure loops during validation, while neural decompilers are trained to undo optimizations in evaluation; preserving loop structure is explored as an LLM prompting option.Source: §1 · pp. 3–4
• Faultless is substantially more capable than prior techniques for evaluating and validating neural decompilers, and completes 90.1% of realtype equivalence checks in under one second and 96.7% in under two seconds.The paper also contributes a Python implementation and a comprehensive evaluation of completeness, runtime, soundness, and use with state-of-the-art models.Source: §1 · p. 4

2 Related Work

• Neural decompilation studies seek to reconstruct source from binaries, while program-equivalence work supplies methods for checking whether transformed programs preserve behavior.The paper frames these as the two related areas whose assumptions may not hold for neural decompilation.Source: §2 · p. 4, §2.1 · p. 4

2.1 Neural Decompilation

• Neural decompilation research moved from recurrent, tree-based, and graph models to transformer-based systems, including larger models and approaches targeting assembly or user-defined types.idioms uses interprocedural context to predict user-defined type definitions.Source: §2.1 · p. 4

2.2 Program Equivalence

• Program-equivalence methods handle loops through synchronization, bounding, external information, or heuristics, while translation-validation approaches also use loop unrolling, compiler information, or black-box strategies.Other approaches include constrained Horn clauses, equality saturation, symbolic execution, and Boogie-based summaries; their stated limitations include execution-data demands, computational cost, manual rules, or incomplete loop handling.Source: §2.2 · p. 5

3 Faultless

• Faultless takes two functions and returns an equivalence proof result, with the compiler and symbolic interpreter run for each function before their execution contexts are compared.The proof result can be “equivalent” or “unable to show equivalent.”Source: §3 · p. 6
• The proof system has three components: a compiler, a symbolic interpreter, and a proof engine.The compiler converts code to an intermediate representation, the interpreter records symbolic execution information, and the proof engine uses it to construct a proof when possible.Source: §3 · p. 6
• A failure to prove equivalence does not necessarily distinguish a nonequivalent pair from an equivalent pair that Faultless cannot prove equivalent.The paper sometimes refers to “unable to show equivalent” as “nonequivalent” for convenience.Source: §3 · p. 6

3.1 Defining Equivalence

• Faultless models inputs and outputs beyond parameters and return values, including pointer-reachable memory, global variables, and function calls.Its broad functional-equivalence framing captures values read or written through these parts of program state.Source: §3.1 · pp. 6–7
• Equivalent functions must return the same values and preserve relevant heap state reachable from return values and arguments, as well as mapped globals and callees under equivalent conditions.The criteria also require matching callee arguments and reachable memory, and a consistent bijective mapping between function and global names.Source: §3.1 · p. 7
• Faultless does not require equivalent side channels or exploit-relevant stack layouts, and does not require side-effect-inducing expressions to occur in a particular order.Without call context, conservatively treating every callee as side-effecting and as accessing every global would make checking brittle.Source: §3.1 · pp. 7–8
• Options narrowly loosen equivalence conditions to accommodate common decompiler patterns that would otherwise produce trivial nonequivalence results.The options are derived from a taxonomy of C decompiler fidelity issues.Source: §3.1 · p. 7, Table 1 · p. 8
• The current implementation has soundness limitations, so functions with different outputs for the same inputs may be judged equivalent.The paper discusses these limitations further in Section 6.1.Source: §3.1 · p. 8

3.2 Execution Model

• Static symbolic execution merges incoming stack, heap, and path-condition states when paths converge, avoiding separate execution of each path to completion.The interpreter executes basic blocks and queues a successor once all its predecessors have final states.Source: §3.2 · pp. 8–9

3.2.1 Loops.

• At loop heads, Faultless abstracts variables changed by the loop with symbolic φ-variables, allowing execution to proceed despite the control-flow cycle.Natural-loop analysis identifies the loop head and uses SSA φ-instructions to identify mutated variables; unnatural loops created with gotos are unsupported.Source: §3.2.1 · p. 9
• Loop φ-variables can represent multiple dynamic values across iterations, while corresponding post-loop φ-variables represent singular values after the loop terminates.Faultless distinguishes mediloop φ-variables, which model an arbitrary loop iteration, from post-loop φ-variables.Source: §3.2.1 · pp. 9–10
• The memory model represents each written heap variable with an address-space graph, whose nodes record memory states at points in the code.Address Mapping objects connect a base address to a graph node; each written variable has its own graph.Source: Figure 4 · p. 10

3.3 Memory Model

• The stack and heap map base addresses to unbounded symbolic address spaces whose immutable graphs preserve writes, branch-specific histories, and snapshots of memory state.Join nodes encode divergent write histories after paths merge.Source: §3.3 · pp. 10–11

3.3.1 Reading.

• Symbolic-index reads distinguish overlap, where a write may contribute, from coverage, where it supplies every value the read can request; partial matches use conditional values and recursive history search.For loop φ-variables, coverage quantifies over read values and requires corresponding write values under the write condition.Source: §3.3.1 · pp. 11–13

3.3.2 Context Independence, Progenitor Variables, and Derived Variables.

• Without calling-context values, Faultless creates fresh symbolic values for unread memory locations and derives further variables from these and other progenitor variables.Progenitors include parameters, φ-variables, calls, globals, and uninitialized locals; corresponding progenitors can be mapped across functions.Source: §3.3.2 · p. 14

3.3.3 The Stack and Compiler Independence.

• Stack variables occupy separate unbounded address spaces, avoiding assumptions about stack-frame layout, although ordinary local-variable accesses usually use index 0.At index 0, each write covers each read, so the read returns the last value written.Source: §3.3.3 · pp. 14–15

3.3.4 Addressability.

• Faultless permits integer values as base addresses for decompiled pointer casts and determines addressability from use, while rejecting sums of two integer addressable expressions.When one operand is a pointer and the other an integer, the pointer supplies the base address; storing through a non-addressable lvalue is an execution error.Source: §3.3.4 · pp. 15–16

3.4 The Compiler

• Faultless generates a high-level three-address IR that preserves source-level detail and builds the control-flow graph directly during IR generation.Its compiler also parses and models types, unlike the type-agnostic Codealign compiler on which it is based.Source: §3.4 · p. 16

3.4.1 Type Deduction.

• Type deduction applies C’s promotions, conversions, casts, and assignment rules to infer temporary types, while accommodating decompiler placeholder types as supertypes of same-sized primitive types.The API can specify size-based types such as _QWORD and undefined8.Source: §3.4.1 · p. 16

3.4.2 Type Inference.

• Type inference constrains domains of possible types from usage and propagates constraints to a fixed point, then uses preferences when several types remain possible.After inference, type deduction runs again to propagate inferred global-variable and function-signature types through temporary variables.Source: §3.4.2 · p. 17

3.4.3 Preparing Loops.

• Before execution, Faultless converts IR to SSA form and analyzes natural loops to identify loop-head φ-instructions and their base-case operands.Natural loops sharing a head are merged for this analysis.Source: §3.4.3 · p. 17

3.5 The Interpreter

• The interpreter executes SSA-form IR, initializes stack locals and globals with symbolic variables, and logs return-state and call information for the proof engine.Instructions producing results receive unique variables held in registers.Source: §3.5 · p. 17, §3.5.1 · p. 17

3.5.1 Interactions with Memory.

• Declared variables are stored on the stack for address-taking and path merges, while struct fields use ABI offsets, requiring UDT definitions and currently limiting platform independence to x86_64.Compiler-generated temporaries use registers; non-loop ϕ instructions are ignored because stack storage handles path merges.Source: §3.5.1 · pp. 17–18

3.5.2 Executing Function Calls.

• Function calls are treated as uninterpreted, with distinct argument sets receiving unique symbolic variables; optional by-reference modeling is disabled by default, while stack-initializer inference is on by default.The initializer heuristic assigns modification-by-reference variables to uninitialized locals whose addresses are passed to calls.Source: §3.5.2 · p. 18

3.5.3 Entering and Exiting Loops.

• Loops execute once with changing values represented by mediloop ϕ variables, then postloop ˆϕ values are written for later code; exit paths also substitute postloop values.Loop heads execute twice, and break or return exits perform the substitution in both memory and the path condition.Source: §3.5.3 · pp. 18–19

3.5.4 Pre-Execution and Loop Invariants.

• 71.5% of realtype loop-ϕ variables meet the generalized-affine criteria and have at least one invariant inferred.For qualifying updates, Faultless infers loop invariants from the change in a variable; strictly increasing or decreasing changes also yield bounds relative to the base value.Source: §3.5.4 · p. 19

3.5.5 The Heap Replay Buffer.

• The heap replay buffer tracks reads and writes relative to mediloop ϕ variables, replaying writes at the base address so later reads such as head->val return 0.The example records ϕcurrent as corresponding to the initial pointer p0; recursively replayed writes also make head->next->next->val return 0.Source: §3.5.5 · pp. 19–20

3.6.1 Synchronization Graphs.

• Synchronization graphs contain loop-ϕ and call instructions as nodes, with edges representing transitive dataflow or control dependencies between them.The graphs capture dependencies relevant to the free variables in expressions associated with progenitor variables.Source: §3.6.1 · p. 21, Figure 7 · p. 21

3.6.2 Building the Coupling Relation.

• Faultless builds the coupling relation incrementally, starting with independent same-operation nodes and proposing dependent-node pairs as earlier equivalences are proven.This graph-guided process avoids naïvely checking every product-graph pair and revisits conjectures when additional variable relationships become known.Source: §3.6.2 · pp. 21–22
• Call conjectures require equivalent arguments, reachable heap memory, and relevant control conditions; loop-ϕ conjectures compare base and recursive cases, using induction to break dependency cycles.Unproven inductive assumptions and relationships proved from them are revoked.Source: §3.6.2 · pp. 22–23

3.6.3 Heaplet equivalence.

• The heaplet checker tests reachable memory by reading an arbitrary index on each heap and checking equivalence under the coupling relation, using typed rather than untyped-bit extensionality.The checker can allow decompiled code to use the original code's composite type when the two representations use different types.Source: §3.6.3 · p. 23

3.6.4 Global Assumptions.

• Faultless assumes two globals correspond when equating them makes checked expressions equivalent, but rejects the assumption if their terminating values differ.The method addresses the difficulty of aligning globals, which are function inputs and cannot be aligned by how they are computed from inputs.Source: §3.6.4 · p. 23

3.6.5 Checking Equivalence Conditions.

• The final checks cover calls, return values, reachable heaps, and input memory, then require function and global names to form separate bijective mappings.Disjunctive constraints accommodate multiple possible name mappings when equivalent calls have ambiguous alignments.Source: §3.6.5 · pp. 23–24

4.1 Experimental Design

• Two experiments use deterministic transformations and unit tests as complementary oracles, with Codealign’s dependency-based equivalence as the baseline.The deterministic-transformation pairs are equivalent by construction, while passing unit tests cannot rule out untested differences.Source: §4 · pp. 24–25, §4.1 · p. 25

4.1.1 Experiment 1: Deterministic Transformation Oracle.

• Experiment 1 reused realtype pairs, rebuilt with referenced type definitions, and filtered unsupported C features, leaving 1,565 of 2,229 test examples.The experiment also normalized selected printf substitutions and an extra address-of pattern before checking pairs.Source: §4.1.1 · p. 25

4.1.2 Experiment 2: Unit Test Oracle.

• Experiment 2 compared idioms’ codegemma-7b predictions with exebench originals, retaining 881 of 1,741 examples after filtering.The experiment required equivalent function names to better match the unit-test oracle.Source: §4.1.2 · p. 26

4.2.1 RQ1: How complete is faultless?

• Faultless proved equivalent more than 50% of pairs at O0 and around 43–45% at other optimization levels, and agreed with unit tests 87.2% on exebench.It greatly outperformed Codealign on the deterministic-transformation experiment.Source: Table 2 · p. 26, §4.2.1 · p. 27, Table 3 · p. 27
• A 30-pair error review found 17 failures unrelated to Faultless’s novel modeling, four oracle failures, and nine fundamental completeness limitations.The oracle failures were cases where the deterministic decompiler produced nonequivalent code; three of the nine completeness cases reflected limited context.Source: §4.2.1 · p. 27
• Faultless’s soundness limitations caused unsound judgments in less than 1% of exebench cases; only five of six apparent unsound instances were real.One apparent instance resulted from undefined behavior in the test harness; most disagreement reflected incompleteness.Source: §4.2.2 · p. 28

4.2.3 RQ3: What are the runtime performance characteristics of faultless?

• On realtype, Faultless judged 90.1% of examples in under one second and 96.7% in under two seconds.Crash runtimes are excluded from Figure 8 because crashes usually occur before the expensive proof-engine stage.Source: §4.2.3 · pp. 28–29, Figure 8 · p. 28
• Solver queries dominate the slower cases, especially with large synchronization graphs or full reads of large fixed-size arrays.Independent calls can require n^2 equivalence checks; array reads and writes can require 2nm solver queries in the described worst case.Source: §4.2.3 · pp. 28–29

5.1 Experiment Methodology

• The experiments use GPT-5.5 with function-level or neighboring context, and vary optimization level, loop-preservation prompting, and re-prompting.The O2 experiments use that optimization level because Faultless finds it most difficult; scores exclude Faultless crashes.Source: §5.1 · p. 30

5.2.1 RQ4: Evaluation of A Frontier Model.

• GPT-5.5 exceeds 55% evaluation and reaches 73% validation accuracy on unoptimized code, and scores at least 46% evaluation and 72% validation at O2.Validation scores are higher in part because matching an inlined body is easier than reconstructing the original function call and argument order.Source: §5.2.1 · pp. 30–31, Table 4 · p. 31

5.2 Results

• Neighboring context does not improve frontier-model validation scores: accuracy falls from 78.5% to 73.5% at O0 and 74.1% to 72.8% at O2.The authors note that neighboring context can be necessary for complete user-defined type definitions in some cases.Source: §5.2.2 · p. 31

5.2.3 RQ6: The Impact of Loop Structure Preservation.

• Loop-preservation prompting raises validation accuracy from 72.1% to 78.1%, while evaluation scores decrease slightly.The authors report that preservation can help on functions whose loops are affected by loop optimizations.Source: §5.2.3 · p. 32

5.2.4 RQ7: Reprompting Based on faultless Feedback.

• Re-prompting can correct genuine errors, but aggressive matching to feedback may make predictions nearly identical to decompiled code and degrade their quality.The paper describes a corrected missing function call as an example, while warning that the model can revert higher-level field accesses to pointer arithmetic.Source: §5.2.4 · pp. 32–33, Figure 9 · p. 33

• Because program equivalence is undecidable, techniques must trade off soundness, completeness, and utility to end users.Source: §6 · p. 33

6.1 Soundness

• Faultless can report nonequivalent functions as equivalent in several identified cases, reflecting implementation features deprioritized relative to their frequency in the datasets.The authors state that these soundness limitations are not fundamental.Source: §6.1 · p. 33

6.1.1 Heap Base Case and Inductive Disassociation.

• Four of the five real soundness issues in Experiment 2 stem from dissociation between base-case and loop-phi heaps.A base-case heap check misses writes represented by phi variables, so the differing writes in Figure 10 go undetected; checking corresponding phi heaplets is a proposed fix.Source: §6.1.1 · p. 34, Figure 10 · p. 34

6.1.2 Recursive Heap Equivalence.

• Without recursive heap checking, Faultless can miss differences beyond one level of indirection and report the Figure 11 functions equivalent.No such soundness issue appeared in the experiment, but the dataset has few structs; the authors note that many linked-structure functions process one layer at a time or use loop-phi semantics.Source: §6.1.2 · pp. 34–35, Figure 11 · p. 34

6.1.3 Heap Induction.

• Loop induction relies on phi instructions for stack variables, so repeated writes to a fixed heap location can be treated like an if-statement rather than an induction case.Only one instance of heap induction was observed in the soundness experiments; the authors propose adding psi instructions for such heap locations.Source: §6.1.3 · p. 35

6.2 Completeness

• Soundness requires incompleteness: context-independent assumptions leave cases where Faultless cannot prove equivalence.The section identifies several consequential completeness limitations.Source: §6.2 · pp. 35–36

6.2.1 Indirect Dependencies through Memory.

• Equivalent functions can be judged nonequivalent when indirect heap dependencies leave Faultless unable to relate allocation results used in branch conditions.In the example, missing SSA edges prevent it from establishing that the exit calls have equivalent control-flow conditions.Source: Figure 13 · p. 36, §6.2.1 · p. 36

6.2.2 Byte-Level Type Reinterpretation.

• Decompiled code that packs several conceptual values into one value can be rejected as nonequivalent despite matching byte sequences.The example contrasts a four-byte string treated as four values with an integer treated as one.Source: §6.2.2 · pp. 36–37

6.2.3 Composite Globals in Validation.

• Composite globals are difficult to match because decompilation may split one global into separate variables without preserving its boundaries or layout.The original fields are relative to the global’s base, while decompiled qword symbols appear as separate globals; without layout information, equivalence is difficult to prove.Source: §6.2.3 · p. 37

7 Conclusion

• Faultless supports evaluation and validation largely without calling-context or dependency information beyond type definitions, while abstracting over most compiler-level details.Source: §7 · p. 37
• Faultless is substantially more capable than Codealign, an existing program-equivalence technique for neural decompilation.Source: §7 · p. 37
• The authors use Faultless to evaluate model performance, compare modeling approaches, check prediction correctness, and guide improved predictions through re-prompting.Source: §7 · p. 37