Bug #1684: BLAST incorrectly updates lvalue indexes when converting to SSA with recursion enabled! - BLAST - Open-Source Projects

Actions

Copy link

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.

Status:

Closed

Priority:

High

Assignee:

Pavel Shved

Category:

Target version:

2.6

Start date:

08/24/2011

Due date:

% Done:

Estimated time:

Detected in build:

svn

Platform:

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

only_int.c (226 Bytes) only_int.c

Pavel Shved, 08/24/2011 09:56 PM

Related issues 2 (1 open — 1 closed)

Actions

Copy link

Updated by Pavel Shved over 12 years ago

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...

Actions

Copy link

Updated by Pavel Shved over 12 years ago

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.

Actions

Copy link