cucapra/dahlia

Typechecker Issue

Opened this issue · 3 comments

The typechecker catches this

let arr: ubit<10>[10][10];
let perm: ubit<10>[10];

for (let i=0..10) {
    let x = perm[i];
    let y = perm[i+1];
    let v = arr[x][y];
}

however this seems to not be caught

let arr: ubit<10>[10][10];
let perm: ubit<10>[10];

for (let i=0..10) {
    let v = arr[perm[i]][perm[i+1]];
}

Oh odd! Maybe it is not assigning a dynamic index type to the accesses memories?

AffineType check tries to consume the array. Looking at the contents of contentList from getConsumeList bank 0 of the variable arr is consumed. Banks of the variable perm are not consumed.

Surely enough as bank 0 of arr is consumed the type-checker catches the following

let arr: ubit<10>[10][10];
let perm: ubit<10>[10];

for (let i=0..10) {
    let v = arr[perm[i]][perm[i+1]];
    let y = arr[1][2];
}
[Type error] [Line 6, Column 13] Bank 0 for physical resource `arr' already consumed.
    let y = arr[1][2];
            ^

`arr' originally had 1 resource(s).

Previous locations that consumed bank 0:

[5.13] Required 1 resource(s):
    let v = arr[perm[i]][perm[i+1]];
            ^

Last gadget trace was:
[{0}][{0}]
[{0}]

and even

let arr: ubit<10>[10][10];
let perm: ubit<10>[10];

for (let i=0..10) {
    let v = arr[perm[i]][perm[i+1]];
    let y = arr[perm[i+2]][perm[i+3]];
}

Adding a screenshot of the stacktrace from debugging.

https://github.com/cucapra/dahlia/blob/master/src/main/scala/typechecker/AffineCheck.scala#L279-L293

Screenshot 2024-01-10 at 12 15 42 PM

Hm, the problem is that perm[i] needs to imply that all banks in a particular dimension need to be consumed. Currently, it is only saying that one bank is being consumed. This probably needs to be changes in Gadgets.scala or something