Bug #1684
closed
BLAST incorrectly updates lvalue indexes when converting to SSA with recursion enabled!
Added by Pavel Shved over 12 years ago.
Updated over 12 years ago.
Published in build:
9cfb95f
Description
I tried to run a simple program with full-blown alias support (attached):
void err() { ERROR: goto ERROR;}
void mutex_lock(int *a)
{ if (*a == 1) err();
*a = 1;
}
void mutex_unlock(int *b)
{ if (*b != 1) err();
*b = 0;
}
int main()
{ int m;
m = 0;
mutex_lock(&m);
mutex_unlock(&m);
}
Command line:
pblast.opt only_int.c -predH 7 -craig 2 -alias bdd -cref -cldepth 2 -enable-recursion
And it reports that the program in unsafe, which is wrong! However, if I exclude the option -enable-recursion, it reports the program as safe! But this stupid program does not contain any recursive calls at all!
I noticed that the indexes of lvalues converted into SSA form just do not match when the recursion is enabled. Is there a bug in lval_map subsystem?
Gotta investigate this...
Files
I recalled that when I turned on the recursion in ldv, tests demonstrated a couple of unexpected changes I didn't want to elaborate (commit:59cafa). Perhaps, that's what it was...
Hm, this bug dates back to the oldest versions of BLAST.
In lval_map subcomponent (SSA trace conversion), -enable-recursion caused BLAST to treat each call as a recursive one with a clean stack of local variables of the recursive function. I guess, the intent was that only a recursive call cleans up the local variables, but this hasn't actually been implemented. It would be interesting to experiment with this functionality, but since this is of less high priority, I merely have commented out this functionality altogether. BLAST's commit:6bdf1f4.
I currently run regression tests for this fix.
I also opened a separate issue for recursion tracking: feature #1685.
- Status changed from Open to Resolved
- Published in build set to 9cfb95f
The regression spotted in tests back then is now fixed. "Surprisingly", tests proved themselves useful!
The fix is applied in commit:9cfb95f, and is now being tested on QA server.
- Status changed from Resolved to Closed
Both tests and big launches work well, closing.
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)
- Target version set to 2.6
Also available in: Atom
PDF