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

[Sean Heelan]

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
-------------- next part --------------
HTML attachment scrubbed and removed