Behavior changes unexpectedly? without a `---`.

[cgyurgyik]

This arose from Futil #356.

Command

fud e f.fuse --to dat -s verilog.data f.data

Program

decl a: bit<32>[4];

let n: ubit<6> = 4;
let m: ubit<6> = 0;
---

while (m < n) {
  let i: ubit<6> = 0;
  while (i < m) {
    let end: ubit<6> = i + 1; // This needs to be using `i`, otherwise the behavior isn't re-produced.
    ---
    let j: ubit<6> = 0;

    while (j < end) {
      let current: bit<32> = a[j];
      ---
      a[j] := current + 1;
      ---
      j := j + 1;
    }
    ---
    i := i + 1;
  }
   --- // The `---` that is toggled.
  m := m + 1;
}

Data

{
  "a0": {
    "bitwidth": 32,
    "data":  [ 0, 0, 0, 0 ]
  }
}

Expected

{ "a0": [ 3, 1, 0, 0 ] }

Actual (with --- before m := m + 1)

{ "a0": [ 3, 1, 0, 0 ] }

Actual (without --- before m := m + 1)

{ "a0": [ 6, 3, 1, 0 ] }

I'm not entirely sure what is wrong yet; I still need to do some digging.

[rachitnigam]

Further minimizing the program:

let n: ubit<6> = 4;
let m: ubit<6> = 0;
let i: ubit<6> = 0;

while (m < n) {
  while (i < m) {
    let end: ubit<6> = i + 1;
    let j: ubit<6> = 0;
  }
  m := m + 1;
}

The problem seems to be that the sequentialize pass does not add a --- between while (i < m) { ... } and m := m + 1.

[rachitnigam]

Thanks for reporting this @cgyurgyik. A good rule of thumb for finding these kinds of issues: if a program type checks without --lower, you should never have to add any "fake" ---. The compiler should do that for you.

Since --- slow down the programs by sequentializing statements, it is always a good idea to minimize them by just running the compiler without --lower. If you run into any more of these, please report them too!

[cgyurgyik]

Thanks for reporting this @cgyurgyik. A good rule of thumb for finding these kinds of issues: if a program type checks without --lower, you should never have to add any "fake" ---. The compiler should do that for you.

Since --- slow down the programs by sequentializing statements, it is always a good idea to minimize them by just running the compiler without --lower. If you run into any more of these, please report them too!

Ok good to know. Here, I initially wasn't sure whether this was part of a pass, or whether it was required by me, the programmer, to place the ---. Hence, the question mark.

[rachitnigam]

Yeah, that’s the thing I’m clarifying—the dahlia type checker will tell you when you need to put in —- by giving resource usage errors. Everything else is supposed to be the pass’s job.

of course, adding —- is a useful debugging trick when the pass is doing something unexpected.

[sampsyo]

Indeed! To put it ever so slightly differently, --- "should" never affect program semantics, i.e., the output. (Removing --- should never change the output, although it can make a program not type-check. Adding --- to a well-typed program should neither change the output nor cause a type error.) If it does, that's a compiler bug.