Records + BufferMemoryIO breaks capability checker

[sgpthomas]

This program doesn't type check with the BufferMemoryIO pass turned on:

record point {
  x: bit<32>;
  y: bit<32>
}

decl shape1: point[2];
decl shape2: point[2];
decl result: point;

let X: bit<32> = 0;
let Y: bit<32> = 0;

for (let i: bit<1> = 0..2) {
  let x = shape1[i].x + shape2[i].x;
  let y = shape1[i].y + shape2[i].y;
} combine {
  X += x;
  Y += y;
}

let out: point = { x = X; y = Y };
result := out;

However, this generates the following code, which does type check.

record point {
  x: bit<32>;
  y: bit<32>;
}
decl shape1: point[2 bank 1];
decl shape2: point[2 bank 1];
decl result: point;

let X : bit<32> = 0;
let Y : bit<32> = 0;
{
  let i : bit<1> = (0 as bit<1>);
  ---
  while ((i <= (1 as bit<1>))) {
    let shape1Read0 = shape1[i];
    let shape2Read0 = shape2[i];
    ---
    let x = (shape1Read0.x + shape2Read0.x);
    let shape1Read1 = shape1[i];
    let shape2Read1 = shape2[i];
    ---
    let y = (shape1Read1.y + shape2Read1.y);
    ---
    X += x;
    Y += y;
    ---
    i := (i + (1 as bit<1>));
  }
}
let out : point = {
  x = X; y = Y;
};
result := out;

I don't know where the problem is exactly.

[rachitnigam]

The input program doesn't type check for a trivial reason: you're re-binding x in the for loop. Can you give an example that doesn't type check on master but should? The second program also type checks on master.

The first example also type checks on the buffer_memory branch. Can you give examples to reproduce the error?

[sgpthomas]

I fixed the examples, for some reason I lost all the capitilzation when I copied over the examples. sorry about that. The other thing is that I fixed this by not using separating the reads into a separate logic time step. However, if you change the construct function at 'BufferMemoryIO.scala:51' to return CSeq instead of CPar, then this bug happens. I'm concerned that this pass is changing the AST in some way that breaks future passes. Using CPar fixes the issue, but it may not fix the root cause of the issue.

I don't think this is an important issue to solve right now though.

[rachitnigam]

Doesn't seem to happen on master which includes a part of the BufferMemoryIO pass.