driller icon indicating copy to clipboard operation
driller copied to clipboard

Driller generated wrong constraints

Open u609 opened this issue 5 years ago • 0 comments

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

u609 avatar Mar 18 '19 14:03 u609