Pathing

In order to symbolically execute multiple basic blocks at a time, we are required to create some sort of bathing strategy since the end of the basic block necessitates a decision about what to execute next. For all bathing strategies we first generate a control flow graph (CFG). Perhaps we want to exhaustively symbolically execute the entire program, and thus enumerate all possible end states.* One example of a pathing strategy would be to symbolically execute each basic block, and upon reaching the end of the block, check the satisfiability of taking each path.** The way the REIL instruction handlers are implemented, the flag registers are already set up as a 1 bit bit vector with conditions based on a Z3 AST. Therefore, if you need to check satisfiability of choosing a particular path you can simply add the constraint on the zero flag being 1 and solve for satisfiability using Z3.

--Finish--

*This would of course be a quick lesson in the meaning of path explosion, but it will serve as a fine example.

**I rely on Z3 for all constraint solving capabilities of reilex.