InvariantValueRedirection: divert invariant theta IO states

[phate]

It should always be possible to divert the IO state of a theta node (if it is invariant). In C(++), it is guaranteed that loops without side-effects, i.e., the IO state is invariant, always have to terminate as they are otherwise considered UB under the language's forward progress rules.

[phate]

@sjalander @haved The code for the problematic benchmark looks like this:

int kernel(in_int_t a, in_int_t b) {
  // Finding K, where K is the greatest power of 2 that divides both in0 and
  // in1. for (int k = 0; ((in0 | in1) & 1) == 0; ++k)
  unsigned k = 0;
  while (((a | b) & 1) == 0) {
    a >>= 1;
    b >>= 1;
    k++;
  }

  // Dividing in0 by 2 until in0 becomes odd
  while ((a & 1) == 0)
    a >>= 1;

  // From here on, 'in0' is always odd.
  // If in1 is even, remove all factor of 2 in in1
  while ((b & 1) == 0)
    b >>= 1;

  // Now in0 and in1 are both odd. Swap if necessary so in0 <= in1, then set in1
  // = in1 - in0 (which is even).
  while (b > 0 && ((b & 1) == 0)) {
    b = b - a;
  }

  // Restore common factors of 2
  return a << k;
}

The purpose of it is to use Stein's algorithm for computing the gcd. However, looking at the code, I have my suspicions that it might not be correct. The function returns a<<k, but the last two loops neither contribute to a nor k, i.e., they are useless computations. @sjalander Where is this test case taken from?

[phate]

@sjalander This is the benchmark I was talking about. Where is it from?

[sjalander]

@phate
It seems to be from here
EPFL-LAP/dynamatic@67940c7#diff-2e39c5a9b0fdf5284bfc776f7f51461c56e798be48ff27d38f439a76f689b8f5

But it has been updated since then and dynamatic now use the following version
https://github.com/EPFL-LAP/dynamatic/blob/8f356fd98517d12e7b29b6994e1d5e628be39268/integration-test/gcd/gcd.c

[sjalander]

@phate
We don't have a strong motivation for why this specific benchmark must be part of the test suit. We could simply remove it to get this PR merged.