|
|
|
|
|
|
by pag
2712 days ago
|
|
|
The Remill [1] machine code to LLVM bitcode binary translator lifts procedural code into an SSA form (LLVM's) and abstracts over the modelled program's memory using small step semantics that also benefits from SSA form. The way it works is that "memory" is just another value, and writes to memory are applied through function calls which return the new value of memory, and reads to memory are calls which accept the current memory value. This document describes it visually [2]. [1] https://github.com/trailofbits/remill [2] https://github.com/trailofbits/remill/blob/master/docs/LIFE_... |
|
|