[klee-dev] how to dampen ktest exuberance with symbolic index into symbolic array

[Richard Rutledge]

Thanks Dan and Christian!

Adding klee_assume is a no-go because that would require either manual 
inspection/modification of the source code or heavy duty program analysis.

I'm evaluating a change to executeMemoryOperation that appears to 
implement the behavior I need (succinctly drive program traces without 
concern for potential defects). I added the following to 
executeMemoryOperation:

...  ref<Expr> offset = mo->getOffsetExpr(address);

     bool inBounds;
     solver->setTimeout(coreSolverTimeout);

     // RLR: probably not the best way to do this
     ref<Expr> mc = mo->getBoundsCheckOffset(offset, bytes);
     bool success = solver->mustBeTrue(state, mc, inBounds);

     if (AssumeInboundPointers && success && !inBounds) {

         // not in bounds, so add constraint and try, try, again
         klee_warning("cannot prove pointer inbounds, adding constraint");
         ExprPPrinter::printSingleExpr(llvm::errs(), mc);
         addConstraint(state, mc);
         success = solver->mustBeTrue(state, mc, inBounds);
     }

     solver->setTimeout(0);
     if (!success) { ...


On the test code below, klee without the new option generates 183 test 
cases. With the option, it generates two.


On 01/10/2017 05:20 PM, Cristian Cadar wrote:
> Hi Richard,
>
> If adding klee_assume's is an option, that's indeed the easiest thing 
> to do, as Dan suggests.  You can also reduce the number of object 
> resolutions as described by Dan, but you risk missing the case where 
> the pointer is resolved to the buffer you're indexing.
>
> One possible solution is to perform pointer tracking, as in our 
> previous system EXE.  This fails to work as indented in some cases 
> such as pointer/integer conversions, but works well in the general case.
>
> Best,
> Cristian
>
> On 10/01/2017 19:39, Dan Liew wrote:
>> Hi Richard,
>>
>> On 10 January 2017 at 00:19, Richard Rutledge <rrutledge at gatech.edu> 
>> wrote:
>>> Consider the following program:
>>>
>>> //-----------------------------------------------------------------
>>> #include <stdlib.h>
>>> #include <klee/klee.h>
>>>
>>> #define BUFFER_SIZE 16
>>>
>>> int main(int argc, char *argv[]) {
>>>
>>>   char *buffer = malloc(BUFFER_SIZE);
>>>   int index;
>>>
>>>   klee_make_symbolic(buffer, BUFFER_SIZE, "buffer");
>>>   klee_make_symbolic(&index, sizeof(index), "index");
>>>
>>>   if (buffer[index] == '\0') {
>>>     return 1;
>>>   }
>>>   return 0;
>>> }
>>>
>>> //-----------------------------------------------------------------
>>>
>>> Given this program, klee generates approx 180 test cases (the actual 
>>> number
>>> seems to vary). I understand from prior correspondence here that 
>>> klee forks
>>> a path for each object which can be referenced. The forking occurs in
>>> Executor::executeMemoryOperation().
>>>
>>> My objective is to only generate inbounds values of buffer and index 
>>> that
>>> induce each of the two paths through the program. My attempts to modify
>>> AddressSpace::resolve to only return the single desired memory 
>>> object have
>>> so far been disappointing (i.e. abject failure).
>>>
>>> Any suggestions as to how I should proceed?
>>
>> For this particular program you could add
>>
>> ```
>> klee_asume(index >= 0);
>> klee_assume(index < BUFFER_SIZE);
>> ```
>>
>> before doing any indexing.
>>
>> If you want KLEE to always be in bounds you'll have to modify KLEE. It
>> sounds like you're looking roughly in the right area but this is a
>> part of the code I've not looked at in detail.
>>
>> Looking at a glance what you need to change is
>> `Executor::executeMemoryOperation()`. You can see that it tries to
>> resolve to check if the pointer can resolve to a single memory object
>> (`AddressSpace::resolveOne()` then a few additional checks). If it
>> possible for the pointer to be out of bounds then an unbounded search
>> using `AddressSpace::resolve()` occurs. You can limit the bound by not
>> passing `0` as `maxResolutions` (arguably that should be a command
>> line option that defaults to 0). You could also just delete this code
>> and fork once and on the forked copy add the constraint that the
>> pointer doesn't resolve to the previously found object and then
>> terminate it as an error state for being out of bounds.
>>
>> To be honest I find the code very hard to follow because the
>> ImmutableTree that stores the memory object is basically not documents
>> so I have no idea why the search in `AddressSpace::resolveOne()` is
>> done the way it is).
>>
>> HTH,
>> Dan.
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev