Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Driller generated wrong constraints #72

Open
u609 opened this issue Mar 18, 2019 · 0 comments
Open

Driller generated wrong constraints #72

u609 opened this issue Mar 18, 2019 · 0 comments

Comments

@u609
Copy link

u609 commented Mar 18, 2019

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant