How to backtrace a path

[jingde liu]

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?

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?

Any help is truly appreciated.

Thank you very much.

Jingde

[jingde liu]

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?

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?

Any help is truly appreciated.

Thank you very much.

[Daniel Liew]

Post by jingde liu
Hi everyone,
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.

Post by jingde liu
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