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

2017-01-11 Thread 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 offset = mo->getOffsetExpr(address);

bool inBounds;
solver->setTimeout(coreSolverTimeout);

// RLR: probably not the best way to do this
ref 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  
wrote:

Consider the following program:

//-
#include 
#include 

#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(, 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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


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

2017-01-10 Thread Cristian Cadar

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  wrote:

Consider the following program:

//-
#include 
#include 

#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(, 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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


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

2017-01-10 Thread Dan Liew
Hi Richard,

On 10 January 2017 at 00:19, Richard Rutledge  wrote:
> Consider the following program:
>
> //-
> #include 
> #include 
>
> #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(, 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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev