[klee-dev] (Re)implementing a randomized fork

[Chengyu Zhang]

Hi Sean,
   You could try random search strategy builded in KLEE with the command:
klee -search=random-state your_file_name.bc.
I think this feature would achieve your goal. If the strategy doesn't work
or can't satisfy you, you could inherit the Searcher Class in
/lib/Core/Searcher.cpp & /lib/Core/Searcher.h to implement your strategy
and register in /lib/Core/UserSearcher.cpp.
   If you have any question about how to implement an own Searcher, you can
ask me.

Cheers,
Chengyu

2017-01-18 5:30 GMT+08:00 Sean Heelan <sean.heelan at gmail.com>:

> Hi,
>
> For various reasons a randomised fork would be beneficial when using
> batched searching. In case it isn't apparent, what I mean by a 'randomised
> fork' is randomly selecting whether the conditions for the true side of a
> branch or the false side are applied to the current state. At present the
> current state is always updated to represent the true side of the branch.
>
> It appears that there used to be such an option to KLEE, but it is now
> gone.
>
> My first attempt at reimplemting it involved the following modifications
> to Executor::fork around line 943:
>
> ```
>     if (forkDist(mtRandEngine)) { // generate randomly a 0 or 1
>       falseState = &current;
>       trueState = falseState->branch();
>       addedStates.push_back(trueState);
>     } else {
>       trueState = &current;
>       falseState = trueState->branch();
>       addedStates.push_back(falseState);
>     }
> ```
>
> I assumed this would work, and the current state would be updated with the
> correct conditions accordingly. When testing it seems like this breaks the
> process tree, as after a while the following call in Executor::fork
> triggers an assertion failure
>
> ```
>     std::pair<PTree::Node*, PTree::Node*> res =
>       processTree->split(current.ptreeNode, falseState, trueState);
> ```
>
> The assertion failure is in `split` and is because current.ptreeNode.left
> is not null.
>
> I hacked around this by simply removing that code (and all other ptree
> functionality), but then started getting failures in
> executeMemoryOperation. At this point I stopped, as I clearly don't
> understand the ramifications of my changes and I was hoping someone could
> help with that! Any suggestions as to where I've gone wrong would be
> appreciated.
>
> Cheers,
> Sean
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>


-- 
张枨宇   Chengyu Zhang
East China Normal University
School of Computer Science and Software Engineering
Tel: +86 18685412181
Mail: dale.chengyu.zhang at gmail.com
-------------- next part --------------
HTML attachment scrubbed and removed