Blogs / Compiler theory

From Graphs to Code: The Compiler Theory Inside HydIR

The hard part of lifting is deciding what every value means on every incoming edge. Control-flow graphs and fixed points make that question precise.

Suppose we already know how each supported machine instruction changes registers and flags. That still does not give us a compiler. A register can be assigned on one branch and left untouched on another. A loop can carry yesterday's value into today's iteration. A return may be reachable through a path on which its result was never initialized.

The missing structure is a graph, and the missing reasoning is dataflow analysis. HydIR's native pipeline expresses those ideas through MachineIR, StateIR, FunctionIR, and CIR. Its scalar compatibility backend offers a particularly small worked example: each recovered instruction becomes an LLVM block, with incoming machine values represented by explicit phi nodes.

We will use that scalar example to derive initialization and SSA, then connect the construction to the native pipeline's memory effects and structured C. The mathematics companion derives the arithmetic carried by the graph. Here the central question is which values are available along which edges, and how to preserve them when the representation changes.

Recovery is a claim about a region

A symbol can provide an entry address $a$ and a byte extent $n$. Alternatively, the analyst can supply both. These define a region:

The 4,096-byte bound belongs to the scalar compatibility lifter. Native discovery has different limits, including a 64 KiB per-function byte bound in the inspected revision. An extent is a recovery boundary, not evidence that every byte inside it belongs to an executed instruction or that the selected function has a particular prototype.

On x86, instructions have variable lengths. Decoding at the wrong offset can produce a plausible but different instruction stream. A lifter therefore needs more than a list of mnemonics: it must commit to instruction boundaries and explain how each boundary was reached.

The scalar backend's recover_bounded function, used by recover, begins with the selected entry in a queue. It decodes an instruction, classifies its semantics, assigns ownership of its bytes, and queues its successors. For the call-free direct-control-flow example:

Every successor must lie in $\Omega$. The ownership map assigns each decoded byte to exactly one instruction start. If the intervals of two distinct recovered instructions overlap, recovery fails:

This rejects a branch into the middle of an already recovered instruction, regardless of which decoding is encountered first. Indirect edges cannot be resolved by this successor rule, so the scalar path rejects them. The native pipeline can recover some bounded indirect target sets; the jump-table article explains why it also preserves an unresolved default.

The result is a directed graph $G=(V,E)$ with instruction addresses as vertices. “Reachable” here means reachable by traversing recovered edges. The pass follows both conditional successors without first proving that their branch predicates are satisfiable. It can therefore include paths that no input will actually take.

That distinction will matter later. A structurally conservative graph can cause an initialization check to reject a function whose unsafe-looking path is infeasible. Rejecting such a case is a precision limit, not permission to silently remove the path.

The maximum fixture as a graph

Consider the same five-instruction unsigned maximum used in the introductory walkthrough:

movq %rdi, %rax
cmpq %rsi, %rdi
jae  .Ldone
movq %rsi, %rax
.Ldone:
ret

Let us name its instruction nodes $m,c,j,u,r$: initial move, comparison, jump, update, and return. The graph is:

A conventional compiler would often group consecutive instructions into larger basic blocks. HydIR's scalar LLVM backend instead creates one block per instruction. This produces more labels and more phi nodes, but preserves a simple correspondence between an address, its state transformer, and its incoming state. Native MachineIR uses its own block representation; one LLVM block per instruction is not a rule for every HydIR pipeline.

The return does not need to remember why a predecessor was selected. It needs the value of RAX from the predecessor that was actually executed. Before generating that selection, however, the lifter must establish that a value exists on every incoming path.

Definite initialization is a must analysis

Let $\mathcal U$ be the scalar backend's field universe: fourteen registers, four flags, and eight stack slots. At each instruction node $v$, define $D_v^{\mathrm{in}}$ and $D_v^{\mathrm{out}}$ to be sets of fields known to be initialized before and after executing that instruction.

Its physical SysV entry model supplies six integer argument registers:

The maximum example uses only the first two. Let $\operatorname{Def}(v)$ contain fields established by the instruction and $\operatorname{Kill}(v)$ contain fields whose old values cannot be carried through. The transfer function is:

Ordinary moves have an empty kill set. An allowed direct call kills caller-clobbered fields and establishes its modeled return value in RAX. Carrying the old flags through that call would create false guarantees. Stack slots enter the same analysis only after a separate stack-frame proof has identified their accesses.

The interesting operation is the join. To be definitely initialized at $v$, a field must be initialized on every incoming edge:

The intersection over an empty predecessor set is $\mathcal U$. Thus the external entry contributes $\mathcal I$ even when the entry node has a loop backedge. Treating the function entry as “whatever the backedge provides” would wrongly allow a loop to invent its own initial values.

For unsigned maximum, the initial move defines RAX. CMP defines all four flags. JAE preserves the fields, and the optional second move redefines RAX. Both paths reaching the return therefore include RAX in their outgoing sets.

Now remove the first move. The update path still defines RAX, but the direct branch to the return does not:

The return must be rejected. Using a union at that join would establish only that RAX is initialized on some path, exactly the wrong claim.

Once the fixed point is computed, HydIR checks each instruction's declared reads:

The implementation represents field sets as bit masks, so this becomes reads & !incoming == 0. Read and write masks come from the shared instruction effects; the graph layer adds stack-slot and allowed-call dependencies. Getting those masks right is part of the semantic model, not a consequence of the fixed-point algorithm.

Why loops need a fixed point

On an acyclic graph, a topological traversal can propagate information forward once. A loop destroys that order: a node's incoming set depends on a predecessor whose incoming set depends on the node itself.

Collect all incoming and outgoing sets into a product domain:

ordered componentwise by set inclusion. Intersection, removal of a fixed kill set, and union with a fixed definition set are monotone. The equations define a monotone function $F:\mathcal D\to\mathcal D$.

HydIR initializes the sets to $\mathcal U$ and repeatedly scans the graph, applying the equations until nothing changes. In mathematical notation, a simultaneous version of the same iteration is:

The implementation updates in place rather than taking a fresh simultaneous snapshot. Monotonicity and repeated complete scans still take the finite descending process to the greatest fixed point of these equations.

There are 26 field bits in each incoming and outgoing set. Across the stored sets, at most $2|\mathcal U||V|=52|V|$ bit removals are possible. This bounds strict state changes, not the total cost of repeatedly scanning predecessors. It explains termination of this analysis without a timeout heuristic.

The optimistic initialization is safe because no reads are approved until convergence. Suppose a loop body defines RAX but the path from entry to its header does not. At the header $h$, with external predecessor $e$ and backedge predecessor $b$:

A field missing from the first entry remains missing at the header. Having a value on later iterations cannot justify its first read.

The fixed point describes all graph paths under these transfer rules. It is not a path-feasibility solver. More precise reasoning could prove some edges infeasible, but that would introduce another analysis with its own correctness obligations.

Making machine state explicit in SSA

Static single assignment form gives every value a unique definition. Registers do not naturally satisfy that property: RAX is repeatedly overwritten. The lifter resolves this by creating a separate SSA name for each modeled field at each relevant block boundary.

For a field $f$ at node $v$, use $x_{v,f}$ for the incoming value and $y_{v,f}$ for the outgoing value. For $f\in D_v^{\mathrm{out}}$, the outgoing name is either a new instruction result or a surviving incoming value:

The entry value is selected from predecessor outputs. If $f\in D_v^{\mathrm{in}}$, HydIR emits the corresponding phi:

At the entry block, an artificial prologue predecessor supplies the six physical arguments; the maximum fixture consumes the first two. Registers and stack slots use LLVM i64; flags use i1. A field that failed the initialization condition receives no invented input value.

Phi is an edge-indexed selection. When control arrives from predecessor $p_i$, the selected value is $y_{p_i,f}$. It is not a runtime function that evaluates all alternatives, and it does not mean “pick whichever operand is defined.” LLVM also requires phi instructions to precede ordinary instructions in a block; incoming uses belong to their predecessor edges. See the LLVM phi specification.

For the maximum fixture, the essential return block has this shape. Names are shortened for explanation:

done:
  %answer = phi i64 [ %a, %branch ], [ %b, %update ]
  ret i64 %answer

The complete raw lift contains many more phis, including single-predecessor phis and fields not ultimately used by the return. It carries the initialized machine state explicitly instead of trying to minimize SSA during construction.

This separates two obligations. The front end produces a traceable representation of state flow. Later passes may simplify redundant values and blocks, provided they preserve the IR's semantics.

Dominance explains the conventional alternative

Why do most compiler discussions introduce dominance when describing SSA? A definition must be available wherever its value is used. A node $d$ dominates $v$ if every path from entry to $v$ passes through $d$:

At a join reached from different definitions, neither definition necessarily dominates the join. A phi introduces a new definition there, with its operands used on the incoming edges.

The dominance frontier records the boundary where a node's dominance stops being strict:

Strict dominance means domination with unequal nodes. This formulation permits a loop header to occur in its own dominance frontier, which is exactly where a loop-carried phi may be needed.

The classic Cytron et al. SSA construction uses dominance-frontier reasoning to place phis. Liveness information can further avoid phis whose results cannot matter.

HydIR's scalar lifter does not implement that placement algorithm. It emits a phi for every definitely initialized field at every recovered instruction block. Comparing these strategies explains the raw IR's size without pretending that the implementation contains a dominance-frontier pass.

For a small, bounded lifter, the explicit construction has a useful audit property: the naming convention links a field's input and output to an instruction address. The tradeoff is redundant structure that later passes may remove.

Native SSA also versions memory and uncertainty

The native pipeline generalizes the state-flow idea without routing C generation through LLVM:

MachineIR retains decoded instructions, locations, control flow, and effect footprints. StateIR assigns versions to state components. FunctionIR carries function and ABI facts into the next representation. CIR supplies statements and terminators for C emission. LLVM is an optional export, as recorded in ADR 0019.

The native component universe includes registers, flags, control state, and memory regions. In the inspected implementation, machine_state_components includes stack, image, TLS, heap, volatile, and unknown memory. These regions are a conservative way of recording dependencies, not a claim that every pointer has been resolved.

For each component $c$, populate_component_ssa allocates a version at a block input and new versions for instruction outputs. A block's component phi records each predecessor's outgoing version:

Entry components start at version zero. That is a name for incoming architectural state, not an assertion that the contents are numerically zero or determined by two scalar arguments. This is a broader model than the compatibility backend's definite-initialization gate.

Memory needs versions because its writes affect later reads. Consider a store followed by a load:

Replacing $M_1$ by $M_0$ in the load needs a reason: for single-byte accesses, proving $a\ne b$ would suffice in this simple memory model. For multi-byte accesses, the byte ranges must be disjoint. A register-level SSA graph alone supplies neither proof.

The equations illustrate the dependency; HydIR's StateIR records component versions and effect descriptions rather than literally storing these mathematical arrays. Its instruction_components function makes a memory write consume the previous region version and produce a new one. Uncertain pointer effects include heap and unknown-memory dependencies. That prevents treating two unexplained accesses as independent merely because their address expressions look different.

Undefined flags and opaque effects also produce versions. An undefined flag must not reuse its old value, and an unknown instruction must not vanish as though it were a no-op. Both Exact and Unknown state operations carry input and output component lists. This lets later views retain the dependency even when its exact arithmetic is unavailable.

There are therefore two distinct questions at a join: which predecessor supplied the state, and how precisely do we know the operation that produced it? Phi nodes answer the first. Semantic fidelity and effect metadata answer the second. Well-formed SSA does not turn an unknown operation into a known one.

Native LLVM export preserves this distinction through exact or opaque effect descriptors and hooks. A verifier accepting the export establishes its LLVM structure, not standalone executable equivalence. It also cannot make a partial native result safe to rewrite. The native unit keeps structural completeness, semantic fidelity, verification status, and rewrite readiness as separate fields.

Leaving SSA requires simultaneous assignments

C has ordinary mutable variables, so an SSA phi must be lowered. On an edge into a block with several phis, the selected incoming values conceptually move into all destinations at once:

Every right-hand expression is evaluated in the state before any phi destination is updated. Ignoring that timing breaks cycles.

For example, an edge may swap two values:

Starting with $(x,y)=(7,11)$, the intended result is $(11,7)$. The naive sequence x = y; y = x; instead produces $(11,11)$, because the second assignment reads the new $x$.

The scalar LLVM-to-C backend's edge function first captures every source in an edge-local temporary, then writes every destination:

uint64_t edge_0 = v_y;
uint64_t edge_1 = v_x;
v_x = edge_0;
v_y = edge_1;
goto L_target;

The general construction is:

Since temporaries are fresh, evaluating one source cannot change another source's value. That directly establishes agreement with the simultaneous update. More elaborate out-of-SSA algorithms can reduce copies and temporary storage; the simple construction makes the semantic argument short.

Incoming edge: (x, y) ← (y, x)

The copies are emitted inside the chosen branch arm before its goto. Thus each arm has its own edge semantics. There is no requirement to guess an original source-level if or while merely to emit correct direct control flow.

The C parser also checks that every phi's predecessor set matches the graph's predecessor set. An operand from a nonexistent block, or a missing operand for a real edge, cannot be treated as an optional annotation.

Optimization follows the semantic model

A raw lift is a starting representation. It may contain copies expressed as addition by zero, flag calculations whose results are never consumed, and blocks that exist only to preserve instruction boundaries.

The scalar LLVM experiment's transform module allows up to four distinct named passes: instcombine, sccp, simplifycfg, and dce. That experiment requires LLVM opt version 14.0.6, retains raw/before/after artifacts, and runs verifier checks around the transformations. These are not prerequisites for native C emission.

These passes answer different questions. Algebraic simplification may replace $x+0$ with $x$. Dead-code elimination can remove a flag computation that has no remaining uses. Control-flow simplification may eliminate an unnecessary jump. Sparse conditional constant propagation reasons about both values and executable edges. The LLVM pass reference describes their intended roles.

A useful simplified SCCP value domain is:

Different constants are incomparable. Here $\bot$ means no value information has yet been established in the propagation process; it is not permission to read an uninitialized machine register. $\top$ means the value is not represented by one known constant. Joining two constant facts gives:

If a branch condition becomes known, the analysis can restrict propagation to the executable successor. A phi then joins values only from edges established as executable by that analysis. This is more precise than merging every syntactic predecessor indiscriminately.

It does not follow that SCCP will reduce maximum of two arbitrary arguments to a constant. The inputs are unconstrained. Optimizations may expose a more compact conditional expression, but the result must remain input-dependent.

The front end's semantic promises are crucial. If a wrapping machine ADD were emitted with an unjustified no-overflow promise, an optimizer could exploit that promise and still be correct with respect to the wrong IR. Correct optimization cannot repair an incorrect initial model.

Similarly, passing opt -passes=verify establishes IR well-formedness, not binary equivalence. The verifier is not independently executing or proving the source machine instructions.

Source-shaped C is another transformation

Labels and gotos are a direct representation of a graph. Recovering familiar syntax adds a separate interpretation step: deciding whether a region corresponds to an if, a loop, or a recognized expression.

For the maximum fixture, the graph and branch equations justify:

return arg0 >= arg1 ? arg0 : arg1;

That justification depends on the whole relevant shape: which comparison defines CF, which jump reads it, which path writes which value, whether another operation changes the result, and where the paths rejoin.

The scalar emit_structured_c implementation validates the grammar, then uses matches_unsigned_max to follow the relevant control and value dependencies. It walks from the prologue to the branch, resolves copies to find the unsigned comparison of the two arguments, checks its inversion, and follows each arm to its returned value. The true arm must return the first argument and the false arm the second. Simply containing a comparison and two moves is insufficient.

Native structured C uses graph algorithms over CIR. Its supported shapes include acyclic conditionals, guarded switches, and several loop forms. Postdominators help identify where branch arms reconverge; a backedge $t\to h$ with $h$ dominating $t$ identifies a candidate natural-loop header:

Under the chosen exit convention, $q$ postdominates $v$ when every path from $v$ to the exit includes $q$. Multiple returns need an explicit common exit convention, and nonterminating regions need separate treatment. Postdominance is not itself a proof that a branch or loop terminates.

The native emitter checks the supported region shape before selecting a structured form and retains direct control flow for other cases. Syntactic validity, pattern recognition, and semantic equivalence remain separate claims. A recognizable loop header alone does not justify dropping an exit, an opaque effect, or a state update.

The direct CFG output remains the useful representation for explaining SSA elimination. Its mechanics do not depend on recovering the author's original control structures.

A may analysis joins in the other direction

The scalar lifter's initialization pass asks what is true on every incoming path. HydIR's separate global-effect analysis asks which accesses might occur, including accesses made by direct callees. The word “might” changes the join operation.

Let $\mathcal G$ be the finite set of tracked global references. Represent a summary as a triple of possible reads, possible writes, and an unknown-effects flag:

The join preserves every enumerated possibility:

If $D_f$ is a function's direct summary and $C(f)$ its resolved direct callees, the propagation equation is:

A caller of a function that may write a global must itself carry that possible write. A caller of an unresolved or unknown-effect function must retain the uncertainty.

The unknown flag is essential. In the concrete meaning of the report, $U_f=1$ says that the enumerated addresses are not exhaustive. An empty write set accompanied by $U_f=1$ is not a purity result. In that state, the absence of an address from $W_f$ supplies no negative guarantee about it.

The source distinguishes known RIP-relative global references from unresolved memory behavior. It also treats call/return stack bookkeeping as stack-local under its documented stack contract. Those modeling assumptions belong to the result, not just to an implementation comment.

This pass can report call and memory information even where exact lowering is unavailable. Effect analysis, scalar lifting, and native recovery have different contracts; success in one does not silently establish the guarantees of another.

Recursion is a finite set problem here

Recursion makes effect summaries mutually dependent. If $f$ calls $g$ and $g$ calls $f$, computing each summary once in source order cannot propagate all information.

For an example, let $f$ directly read global $\alpha$ and $g$ directly write global $\beta$:

Starting with the direct summaries and applying the join equations repeatedly gives:

Information only grows. Each tracked reference can enter a read or write set once, and each unknown flag can change from zero to one once. Across $N$ selected functions and $G$ tracked references, there are at most $N(2G+1)$ such additions. Again, this counts strict information changes, not total scanning cost.

The least fixed point is enough because the analysis begins with direct facts and adds only the consequences of the resolved call graph. No widening is needed for this finite domain. This is a small, concrete instance of the lattice-based reasoning developed in Cousot and Cousot's abstract interpretation framework.

A strongly connected component groups functions that can reach one another through calls. Collapsing those components gives an acyclic graph and can guide an efficient schedule. HydIR computes SCC identifiers for its summaries, but the inspected implementation performs repeated global scans; it should not be described as an SCC-scheduled solver.

The contrast with initialization is now precise. Initialization starts at the top and removes unsupported guarantees using intersection. Effect propagation starts with direct possibilities and adds consequences using union. Both terminate because the domains are finite, but the meanings of their sets are different.

Confusing these directions can create a false initialized read or a false claim of purity. The choice of lattice operation encodes the question being asked.

Reproducing the stages

The native stages can be inspected separately for a selected function:

cargo run --locked --bin hydirctl -- lift fixture.elf \
  --function hydir_max2 --ir state
cargo run --locked --bin hydirctl -- lift fixture.elf \
  --function hydir_max2 --ir cir
cargo run --locked --bin hydirctl -- decompile fixture.elf \
  --function hydir_max2 --view low
cargo run --locked --bin hydirctl -- decompile fixture.elf \
  --function hydir_max2 --view unit

For the scalar LLVM compatibility example, use the explicit prototype assertion and a compatible toolchain:

cargo run --locked --bin hydirctl -- cfg fixture.elf hydir_max2
cargo run --locked --bin hydirctl -- lift fixture.elf hydir_max2 \
  --assume-u64x2 --output max2.ll
opt -passes=verify -disable-output max2.ll
cargo run --locked --bin hydirctl -- decompile fixture.elf hydir_max2 \
  --assume-u64x2 --output max2.c

The fixture path in those commands is a placeholder. The repository's demo-local.sh creates its trusted fixtures and exercises the complete local comparison path. demo-corpus.sh adds the scalar corpus. Native differential execution requires Linux x86-64; the project also supplies a Docker demo runner.

Each artifact answers a narrower question than “did we decompile the program?” The CFG records selected instruction boundaries and edges. Initialization checks justify modeled reads. SSA records values per incoming edge. The C emitter translates that graph into a restricted C grammar. The verifier checks LLVM structure. Differential tests compare chosen observations for chosen inputs.

The theory is useful because it identifies the seams between those artifacts. At every seam, one can state the object being preserved, the assumptions under which it is preserved, and the evidence that currently checks it.

Reading the implementation

Implementation descriptions were checked against revision b00835d, and source links are pinned to it. Native and scalar compatibility paths are identified separately.

• hydir-backend/src/cfg.rs: recover_bounded, Node::defs, Node::reads, Node::kills, analyze, and lift_cfg implement scalar graph recovery, initialization, and explicit SSA.
• hydir-decompile/src/lib.rs: lower_state_ir, populate_component_ssa, and instruction_components implement native state flow and component versions.
• hydir-c/src/lib.rs: parse_phi, edge, and emit_c implement the restricted C backend; emit_structured_c is a separate presentation path.
• hydir-transform/src/lib.rs: the pass allowlist, LLVM version check, retained artifacts, and verifier invocations.
• hydir-analysis/src/lib.rs: direct effect collection, union-based summary propagation, uncertainty, and SCC labels.

For the arithmetic inside each state transformer, return to From Bitvectors to Behavior. The graph algorithms preserve values only as faithfully as those local semantics define them.

Download the Markdown and LaTeX source