Docs / VM profiles and host/VPC exploration
Virtual-machine profiles and bounded exploration
Repository reference · blog/content/guides/vm.md · source digest 5ffcf5316dd3
Analyst-scoped VM facts, profile validation, virtual-PC-sensitive node identities, effect declarations, and explicit graph limits.
Host and virtual-PC state stay separate#
HydIR can validate an analyst-scoped VM profile and explore host instructions with a virtual program counter (VPC) in the node identity. This is experimental host/VPC graph recovery, not automatic devirtualization.
Describe the interpreter#
VmProfile v1 binds the binary digest and records an entry, exits, VPC storage, bytecode ranges, context layout, and permitted guest effects. Each fact carries analyst, static-inference, or trace-observation evidence.
| Profile fact | Purpose |
|---|---|
| Entry and exits | Scope the interpreter region |
| VPC | Register or context-offset storage, with optional initial value |
| Bytecode ranges | Bound the bytes treated as VM instruction data |
| Context | Entry register, base register, and extent |
| Guest effects | Declared register/context effects, calls, returns, or disjoint memory |
An assertion that external memory writes are disjoint from VM state is an analyst assumption. It is not evidence that self-modifying bytecode is absent.
Validate before exploring#
hydirctl vm-profile program.elf profile.json
hydirctl vm-explore program.elf profile.json
Construct the profile from the actual binary; addresses and the SHA-256 must match. The CLI bounds the profile JSON to 1 MiB. The profile tests show a complete fixture-backed profile construction using discovered ELF locations rather than hard-coded reusable addresses.
Interpret the graph#
A node key contains a host PC and an optional VPC. Two visits to the same host instruction with different known VPCs can therefore be different nodes. Nodes retain the decoded mnemonic and machine bytes. Edges distinguish next, taken, fallthrough, jump, call, call-return, exit, and unresolved flow.
The current explorer caps the graph at 10,000 nodes and the modeled context at 65,536 bytes. Unsupported instructions and addresses end edges explicitly. Inspect unresolved_edges, hit_node_limit, diagnostics, and observed guest effects with the graph.
profile_validated means the declared profile is internally consistent with the ELF. It does not mean a guest CFG was recovered or that rewriting is safe. The separate guest_cfg_recovered and rewrite_ready fields make those limits visible.