[klee-dev] How to backtrace a path

[Daniel Liew]

On 6 Dec 2013 01:21, "jingde liu" <liujingde2008 at gmail.com> wrote:
>
> Hi everyone,
>
> I have two questions:
>
> 1) The first one is about state backtracking in KLEE. I want to backtrace
the current state to "n" steps before instead of the last step. How should
I do it?

AFAIK KLEE does not support this. Stepping backwards is not
straightforward. Things to consider:

- how does Klee unfork?
- how does klee know what the inverse operation of an instruction is?

I think it would be possible to implement but it would be challenging!

A simpler alternative is if you know what state you would need to step back
to is to keep two copies of ExecutionState. The first copy you execute as
normal ( forwards ). The second copy is left untouched. If you find the
need to jump back then delete the first copy and then use the second copy.

> 2) The second one is about path condition. I want to know the constraint
of each step in the current path. How should I get this information from
the current data structure?

Look at the ConstraintManager inside ExecutionState.

Hope that helps,

Dan Liew
-------------- next part --------------
HTML attachment scrubbed and removed