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