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