#3 original input vars reused after input re-initialization

[Gautam Altekar]

Currently, if the program read()s into the same buffer multiple times, then the same input var is used for both reads. That means that the formula emmitted for the following example will be unsatisfiable:

char a = 'y';
char b;

read(fd, &b, 1); // emit declaration INPUT&b_OFFSETx
if (b == 'x') { // INPUT&b_OFFSETx == 'z'
}
lseek(CUR_POS, -1);
write(fd, &a, 1);
lseek(CUR_POS, -1);
read(fd, &b, 1); // use INPUT&b_OFFSETx
if (b == 'y') { // INPUT&b_OFFSETx == 'y'
}

What should ideally happen, AFAICT, is that an entirely new origin var for b be declared and used after the second read(). For example,

After the first read(): emit decl for INPUT&b_OFFSETx_0
After the second read(): emit decl for INPUT&b_OFFSETx_1

Does this sound right to you? Do you see any complications?

This is important for me because my inputs are shared memory reads. In general, there is no guarantee that subsequent reads to a memory location will have the same value.

[David Molnar]

Logged In: YES
user_id=896370
Originator: NO

I agree - this is a problem, and I agree with your way to fix it. I don't see any complications at this time. I'll add the fix sometime this weekend.

[Gautam Altekar]

Logged In: YES
user_id=1954156
Originator: YES

hardcorebit,

Please assign this bug to me (i.e., don't start on it if you haven't already). My patch is almost ready for review.

Thanks!

[Gautam Altekar]

Logged In: YES
user_id=1954156
Originator: YES

Is there a reason why we need the "OFFSET" field in "INPUT_MEMx_OFFSETy"? Can it be made a comment?

I'm thinking we need a more generic and informative name for input vars, so that it will be easy to associate inputs to corresponding syscall results by looking at the solution file. Something like:

INPUT_MEMw_TYPEx_EIPy_EPOCHz,

where w is the address of the origin , x is the syscall number (e.g., 3 for read) or 0 if the origin resulted from a shared mem access (specific to my stuff), y is the address of the syscall or shared memory read instruction, and z is the number of times the instruction executed.

[David Molnar]

Logged In: YES
user_id=896370
Originator: NO

OK, will do. (You're not in the list of assignees, but treat it as assigned to you until I fix that.)

[David Molnar]

Logged In: YES
user_id=896370
Originator: NO

Ok, assigned to galtekar.

[David Molnar]

Logged In: YES
user_id=896370
Originator: NO

I use OFFSET for creating new test cases from STP answers - I need to know which bytes to change in the original seed file to create a new test case. It would be inconvenient for the OFFSET to be a comment, because then it would not show up in the STP answer and I'd have to go parse the input to STP to map the INPUT assignments to bytes in the original file.

The OFFSET could be optional, however, and only omitted for read() syscalls. That would work fine for me.