[klee-dev] Guided Search - Help

[Andrew Santosa]

Hi Alberto, 
For seeding with file.bout, you can invoke KLEE, for example, in the following way:
klee -seed-out=file.bout -posix-runtime <bitcode file> [symbolic environment options] 
I usually try to provide symbolic environment options (-sym-arg, etc.) that correspond to the concrete arguments I provide gen-bout with. For example, if I provide gen-bout with "arg" as command line argument, I will add -sym-arg 3 as a symbolic environment option. 
You may also want to consider KLEE's -only-seed option to just execute the seed without initiating path exploration. 
I hope this helps. 
Andrew 

Sent from Yahoo Mail on Android 
 
  On Mon, Oct 15, 2018 at 7:53 PM, Alberto Barbaro<barbaro.alberto at gmail.com> wrote:   Hi Andrew,Thanks for your email and PR. So I tested gen-bout on a simple project called first that prints a different message depending on the first byte of file passed as a parameter. I think I did it properly because at the end I had the file.bout file. At this point I was able to use klee-replay with it and have the same stdout. Now I don't know how to use file.bout as a seed. Are you happy to show me a simple example please? I would like to able to use it in conjunction with a new searcher in order to 'execute,' queries at runtime on the code.
Thanks a lot!
Alberto

On Mon, Oct 15, 2018, 01:19 Andrew Santosa <asantosa1999 at gmail.com> wrote:

Hi Alberto, 
Thank you for describing your problem. I had submitted this PR some while ago: 
https://github.com/klee/klee/pull/956
Basically I would use gen-bout implemented in the PR to create a ktest file using concrete inputs, then use the ktest file as a seed. In this way, all inputs will be symbolic, yet the path is the one that would have been executed using the concrete inputs. 
Best, Andrew  
 
  On Sun, Oct 14, 2018 at 8:25 PM, Alberto Barbaro<barbaro.alberto at gmail.com> wrote:   Hi all,I have already asked this in the past and received few suggestions but I was not able to do it. I'm trying to test pngpixel[1] that takes as input an image file. My goal is to execute pngpixel with a real file and subsequently execute pngpixel with a symbolic file and follow the path followed by the first execution.I would like to describe my approach so before spending to much time on it and I can understand if I'm doing it right or not :)
1 - Execute pngpixel enabling -debug-print-instructions=src:file2 - Inside my searcher create a map from instruction.txt so I know which is the next instruction3 - Inside the update() function for my searcher, get the current instruction, get the next instruction,4 - Check for each state in addedStates if the next instruction would be execute at the next step in the state5 - If yes add the state using state.push_back(state) else remove the state ( adding the state to removedStates? )
I'm sure this flow is not optimized but at least is it correct? How would you approach this problem?
Thanks for your timeAlberto
[1] https://github.com/fcoulombe/libpng/blob/master/contrib/examples/pngpixel.c
_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
  

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