Hi all, I am doing research about KLEE recently and I want to record my experimental results and let people easily reproduce my experiment. In detail, I want to keep the same instruction execution sequence in different KLEE execution. For now I am using default searching strategy (random-path & nurs:covnew), and I already write some code to record and reproduce the random number generated by /lib/Support/RNG.cpp in /lib/Core/Executor.cpp and /lib/Core/Searcher.cpp. However, the instructions.txt generated by -debug-print-instructions=src:file is still different every time, which means there is still some randomness. To locate the problem, I applied nurs:covnew strategy and random-path strategy separately to KLEE. The results show that my code works a little (can reproduce most instructions in same sequence with the initial run) on random-path strategy but doesn't work at all in nurs:covnew. Here is my code : https://github.com/klee/klee/compare/master...Chazzzzzzz:master I run klee like this : (1)To record random value (should run first): /home/chaz/klee_original/klee_build_dir/bin/klee -debug-print-instructions=src:file --check-div-zero --optimize --libc=uclibc --posix-runtime -record-executor=true -record-searcher=true -search=nurs:covnew sndfile-convert.bc -normalize -alaw A -sym-files 1 45 out.vox (2)To reproduce : /home/chaz/klee_original/klee_build_dir/bin/klee -debug-print-instructions=src:file --check-div-zero --optimize --libc=uclibc --posix-runtime -replay-executor=true -replay-searcher=true -search=nurs:covnew sndfile-convert.bc -normalize -alaw A -sym-files 1 45 out.vox
For now, I am thinking there may be some other random number generator related to state selection which may influence instruction execution sequence. But I haven't found it yet. Also, it would be a good idea to implement such reproduce interface which can ensure instruction execution sequence since some guys may want to reproduce the experimental result like me. Let me know if you have any ideas about this problem! Thanks in advance! Best, Chaz
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev