[klee-dev] How to deterministic reproduce experimental results (instruction level) of default search strategy

[changze cui]

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
-------------- next part --------------
HTML attachment scrubbed and removed