Hi,
On Fri, 9 Nov 2018 08:38:23 +0000 Alberto Barbaro <[email protected]> wrote: > Thanks for your answer. I still have problem with this searcher anyway. For > me it is not obvious how to select between 10 states. This happens after > the first branch encountered in the code. So at the moment I'm iterating on > all of them and discard it one by one if I encountere an instruction that > is not in instruction.txt. do you think this approach is fine or for > example I should save all the states encountered during the execution with > real input and using them just reexecute the same path but with symbolic > input? sorry, I haven't read the thread about the guided search. I guess what you have now is a trace in instructions.txt of a single state (the run with concrete). And you want to replicate that trace in a second run on symbolic data with a new searcher. Correct? First of all, I'm not sure if this works as the trace in the second run might differ from the first: - imho the setup code for symbolic file handling from POSIX layer should be in the new trace - setup routines for uclibc might behave differently and introduce divergences You have to analyse where the branch happens and if there exist an identical trace among your states. If this is not the case, you could for instance start filtering states beginning with your program's main() etc.. To your question: assuming that this approach works, you need to check if the current instruction of a state is at the correct position in your instructions.txt. The "position" in file is the line number and in your state it should be state.steppedInstructions. If it doesn't match, you can terminate or postpone the state, depending on your use case. If you need to introduce a mitigation as above you obviously have to keep an additional offset per state to fix divergences. Kind regards, Frank >> On Sat, 3 Nov 2018 17:21:02 +0000 >> Alberto Barbaro <[email protected]> wrote: >> >>> Just a quick one. Can I use the same approach for the current state and >>> just remove it? >> >> from a searcher? The current state is only passed in >> Executor::updateStates - so this should be fine. But we still have issue >> #952 (easy to fix) in case sth. goes wrong. _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
