Blogs / Worked example

How HydIR Lifts a 16-Byte Function

Let's take one small function apart. hydir_max2 returns the larger of two unsigned arguments, and its assembly fits in 16 bytes. We will read those bytes, follow the branch HydIR recovers, inspect the LLVM IR and C output, and finish with a finite comparison against the original fixture. Along the way, each stage tells us something different about the function.

Start with the function

Here is the assembly fixture in full:

.globl hydir_max2
.type hydir_max2, @function
hydir_max2:
    movq %rdi, %rax
    cmpq %rsi, %rdi
    jae .Ldone
    movq %rsi, %rax
.Ldone:
    ret

Read it from the top. The first movq puts the first argument in RAX, the return register. cmpq %rsi, %rdi then sets flags as if it had calculated rdi - rsi. If RDI is at least RSI, jae jumps straight to ret; otherwise the second move replaces RAX with RSI. That is unsigned maximum. A signed comparison would give a different answer for some values with the top bit set.

HydIR egui disassembly of hydir_max2 with five instruction addresses and their machine bytes — Decoded bytes in the egui workbench.

Give HydIR a boundary

HydIR begins by reading the ELF file. Its importer accepts little-endian x86-64 ELF up to 64 MiB and records sections, load mappings, symbols, imports, and relocations. That inventory gives the later CFG recovery its function boundaries and file provenance.

For this fixture, the symbol table points to 0x401138 and says the function occupies 16 bytes. That gives the lift a place to start and a boundary it must respect. You can also supply an address and byte count yourself; the demo does this with cfg-at and lift-at after stripping a copy of the fixture. Either way, the CLI needs --assume-u64x2 to assert the SysV AMD64 prototype u64(u64, u64). Those argument types come from us, not from the machine bytes.

Follow the two routes to `ret`

Starting at the declared entry, HydIR uses iced-x86 to decode reachable instructions. It follows direct jumps and both sides of a conditional branch until it reaches returns. Here the jae gives us two routes: take the jump or execute the second move. HydIR checks that both routes stay inside the selected function and that decoded instruction boundaries do not overlap. This function-scoped path accepts up to 4,096 bytes.

The recovered graph has five instruction blocks and five edges. From jae at 0x40113e, the taken edge reaches the return at 0x401147; the fallthrough edge reaches the second move at 0x401144. Both routes end at the same return. The saved CFG includes addresses, original bytes, edge kinds, the binary SHA-256, the symbol extent, and the stated recovery scope. Those details let you check exactly which function the graph describes.

HydIR egui CFG view listing five reachable instructions and the taken and fallthrough edges of jae — The branch has two successors; both reach the return.

HydIR egui inspector showing the 16-byte symbol extent, asserted ABI, and five CFG blocks and edges — Symbol extent, ABI assertion, and recovered CFG counts.

Turn the branch into LLVM IR

The lift now has to represent what each instruction does to machine state. In this scalar subset it tracks five full-width registers, RAX, RDI, RSI, RDX, and RCX, plus ZF, SF, OF, and CF. The two arguments start in RDI and RSI. Before generating IR, HydIR checks which values are definitely initialized at each instruction. At a branch join, a value must be defined on every incoming route before it can be read. Every return route must define RAX.

HydIR gives each recovered instruction an LLVM basic block. A phi node chooses between values arriving from different predecessors. In this example, the comparison sets CF when RDI is below RSI. The jae branch takes the other case, and the phi at the return chooses the right RAX value for the route taken. The IR stays close to registers and flags; it is not trying to recreate the author's source code.

The useful lines from the generated max2-lifted.ll are short enough to inspect:

%cf_out_40113b = icmp ult i64 %rdi_in_40113b, %rsi_in_40113b
%t_40113e_0 = xor i1 %cf_in_40113e, true
br i1 %t_40113e_0, label %b401147, label %b401144
%rax_in_401147 = phi i64 [%rax_in_40113e, %b40113e], [%rax_out_401144, %b401144]
ret i64 %rax_in_401147

The first line computes unsigned carry, the branch tests its inverse, and the phi selects RAX at the join. The full file also carries the other registers and flags; cmp computes ZF, SF, OF, and CF even though this branch uses CF. HydIR leaves nsw and nuw off wrapping arithmetic because the machine instruction did not promise that overflow was impossible.

The C output follows that same graph. It uses labels, gotos, and copies at branch edges. For this comparison, the carry expression compares the two inputs as unsigned values.

Check the result against the fixture

It helps to check more than the shape of the IR. demo-local.sh builds the assembly fixtures, lifts them, emits C, and compares the generated outputs with native execution. It runs LLVM's verifier when opt is available. The script also strips a copy of hydir_max2 and tries the address-and-size path. demo-corpus.sh requires opt and adds 16 scalar functions. With the four distinct functions in the local demo, that makes 20 documented scalar fixtures.

bash scripts/demo-local.sh
bash scripts/demo-corpus.sh

For each output path, validation tries 1,008 controlled input pairs. It compares the lifted runner and compiled C runner with the original fixture, including stdout, stderr, and exit status. Here are fields from one recorded hydir_max2 report:

{
  "cases_attempted": 1008,
  "cases_matched": 1008,
  "cases_mismatched": 0,
  "result": "pass",
  "sandbox": "none; trusted fixtures only"
}

The report records 1,008 matched input pairs. opt -passes=verify checks the LLVM IR structure, while the fixture comparison checks the recorded executions. The validation command uses --trusted-fixture. Run the demos on Linux x86-64, or use the repository's Docker runner on macOS.

What happens beyond this function?

HydIR's global-effect pass works over ELF function symbols and reports hydir_max2 as BOUNDED in this demo ELF. It reports _start as UNKNOWN EFFECTS. These are separate per-function results in the same executable.

HydIR egui global-effects rows marking hydir_max2 bounded and _start unknown effects — Per-function effect status in the max2 ELF.

A second fixture makes that distinction easier to see. The call view resolves direct edges from _start to hydir_parent, then from hydir_parent to hydir_leaf. It has no resolved edge for hydir_indirect. That absence means the view did not resolve an edge there; it is not evidence that no call can occur.

HydIR egui program-call graph with direct edges from _start to hydir_parent to hydir_leaf and a separate hydir_indirect node — Only resolved direct calls become edges.

In the same fixture, hydir_leaf writes hydir_counter in .data. Because hydir_parent directly calls it, the parent's summary includes a possible write at 0x402000. “Possible” matters here: this is a may-write result within the pass's bounded scope.

HydIR egui global-effects view listing hydir_parent calling hydir_leaf and a possible write to .data address 0x402000 — The caller carries the callee's possible global write.

And rebuilding an executable?

HydIR has a separate route for that. demo-recompile.sh exercises three trusted, static freestanding fixtures. It requires complete supported text coverage, bounded mapped data, direct calls and branches, and checked read/write/exit syscall sites and buffers. The rebuilt executable goes into a new directory.

The script compares stdout, stderr, and exit status on selected inputs. Its report records those controlled fixture executions alongside the rebuilt artifacts.