driller
driller copied to clipboard
Driller generated wrong constraints
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