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

[Sean Heelan]

Hi Chengyu,

Thanks for your reply.

Unfortunately that won't help when running in batched execution mode, in
which state selection is only triggered at intervals. So, while random
state selection would achieve the desired post-fork randomness when used
alone, I would guess that any benefit would be offset by the fact that
random state selection as a strategy works rather poorly in comparison to
batching + code coverage + random path.

To be more clear about what I'm trying to solve: when running in batched
execution mode if the following function is triggered multiple times then
it will fork at the `if`, and always take the `return -1`. What I would
like is for there to be equal probability of hitting the code after the if
within foo. Given infinite time and resources and a perfectly functioning
code coverage based heuristic you could say "Oh, but that path will
eventually be scheduled", but those 3 assumptions don't hold in practice
and on all programs. For this reason, introducing some variance in the
forking strategy would be quite useful (in practice I am seeing this
pattern quite frequently preventing code being hit that I know contains
bugs).

```
void foo(int x) { // assume x is symbolic
    if (x) {
       return -1;
    }

    .... // do other stuff
}
```

As a side note, obviously if the function has multiple branches then in
order to achieve an equal probability of each branch target being hit then
we'd need to weight the probability of earlier edges which exit the
function being weighted lower than ones which don't, but I'd settle for
50/50 probability to begin with =)

On Wed, Jan 18, 2017 at 4:02 PM, Chengyu Zhang <dale.chengyu.zhang at gmail.com
> wrote:

> 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