pathexecutor: add methods for computing preimage of states

For given path and T, we compute the condition on states X such
that X -> path -> T are executions of program.