shellphish / driller

Driller: augmenting AFL with symbolic execution!
BSD 2-Clause "Simplified" License
880 stars 163 forks source link

Driller generated wrong constraints #72

Open u609 opened 5 years ago

u609 commented 5 years ago

My test.c

int main(int argc, char *argv[]) {
  char buffer[21] = {0};
  int i;
  int *null = 0;

  read(0, buffer, 20);
  if (buffer[0]=='5'){
     printf("==5\n");
  }
  if(!memcmp(buffer,"7aaa",4)){
     printf("==7aaa\n");
  }
}

My test_driller.py

import driller

d = driller.Driller("./test", b"6")
print(d.drill())

when input_str is b'6',I can get result b'7aaa',as predicted.

and the constraints were :

[<Bool file_0_stdin_0_7_160{UNINITIALIZED}[7:0] != 53>, <Bool file_0_stdin_0_7_160{UNINITIALIZED}[7:0] .. file_0_stdin_0_7_160{UNINITIALIZED}[15:8] .. file_0_stdin_0_7_160{UNINITIALIZED}[23:16] .. file_0_stdin_0_7_160{UNINITIALIZED}[31:24] == 0x37616161>]

But,when input_str is b'5',I can get nothing.

and the constraints were :

[<Bool file_0_stdin_0_7_160{UNINITIALIZED}[7:0] == 53>, <Bool file_0_stdin_0_7_160{UNINITIALIZED}[7:0] .. file_0_stdin_0_7_160{UNINITIALIZED}[15:8] .. file_0_stdin_0_7_160{UNINITIALIZED}[23:16] .. file_0_stdin_0_7_160{UNINITIALIZED}[31:24] == 0x37616161>]

Obviously, this constaints were unsolvable.

I think the first constraint:<Bool file_0_stdin_0_7_160{UNINITIALIZED}[7:0] == 53> should not appear here. How can i fix it? Thanks