LARA

Constant Propagation

  • like initialization, but keeps the value to which it is initialized
\bot, C, potentially non-constant
int a, b, step, i;
boolean c;
a = 0;
b = a + 10;
step = -1;
if (step > 0) {
  i = a;
} else {
  i = b;
}
c = true;
while (c) {
  print(i);
  i = i + step;    // can emit decrement
  if (step > 0) {
    c = (i < b);
  } else {
    c = (i > a); // can emit better instruction here
    // put here (a = a + step), redo analysis
  }
}

Correctness of Constant Propagation

  • concretization function
  • comparison of N-th step of data-flow iteration and N-th step of state exploration