HydIR dragon logoHydIR

Docs / Symbolic exploration with Triton

Symbolic exploration with Triton

Repository reference · blog/content/guides/symbolic.md · source digest 90436ab4115b

Optional runtime setup, symbolic expressions, path conditions, candidate models, and desktop exploration.

Symbolic inputs produce bounded candidate models#

Symbolic inputs produce bounded candidate models1Concrete seed + selected symbolic bytesState and input scope are explicit2Triton expressions + path conditionsTrack supported instruction effects along a bounded path3Solver queryAsk for a model satisfying the selected condition4Candidate input + validationA solver model needs a separate concrete check
A symbolic candidate is evidence under a model and budget, not a claim about every execution.

The optional Triton bridge explores direct paths in a selected x86-64 function and reports symbolic expressions, path conditions, and candidate models. It requires a Python interpreter with Triton installed. doctor checks whether the configured interpreter can import it.

export HYDIR_TRITON_PYTHON=/path/to/python-with-triton
cargo run --locked --bin hydirctl -- doctor
cargo run --locked --bin hydirctl -- triton /path/to/program.elf function_name

In the workbench, Run Triton operates on the selected function. The bottom console accepts a restricted statement set, one entry at a time. Triton exploration is separate from the LLVM and native C paths; explored paths do not establish whole-program equivalence.

HydIR disassembly with decoded machine instructions and a docked Triton symbolic result

The disassembly view places decoded instructions beside a docked Triton result, so the selected function and its symbolic exploration can be inspected together.