-
Notifications
You must be signed in to change notification settings - Fork 50
Open
Labels
C: Prog AnalysisRelated to formal analysis, SMT, etc.Related to formal analysis, SMT, etc.
Description
stage_mem does not consider windows which alias with the buffer that is being staged.
@proc
def foo(a: i32[16]):
c = a[2:6]
for i in seq(0, 4):
c[i] += 1
a[i + 2] += c[i]
stage_mem(foo, foo.find('for i in _: _'), 'a[2:6]', 'b')
outputs:
def foo(a: i32[16] @ DRAM):
c = a[2:6]
b: i32[6 - 2] @ DRAM
for i0 in seq(0, 6 - 2):
b[i0] = a[i0 + 2]
for i in seq(0, 4):
c[i] += 1
b[i + 2 - 2] += c[i]
for i0 in seq(0, 6 - 2):
a[i0 + 2] = b[i0]
which is not equivalent to the original procedure because the write to c[i] aliases with the staged window b.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
C: Prog AnalysisRelated to formal analysis, SMT, etc.Related to formal analysis, SMT, etc.