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.hee...@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 = ¤t;
> trueState = falseState->branch();
> addedStates.push_back(trueState);
> } else {
> trueState = ¤t;
> 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@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.zh...@gmail.com
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
