exo-lang/exo

Reading undefined memory locations

Opened this issue · 0 comments

There is two potential views on this from a front-end prespective:

  1. A strict view: Any read to an undefined memory location, makes the program undefined and by extension unacceptable.
  2. A more relaxed view: A read to an undefined memory location as long as the undefined values don't propagate to the arguments.

Same views on this from the rewrite presepctive:

  1. A stricit view: a rewrite isn't allowed to introduce reads to undefined memory locations.
  2. A more relaxed view: A read to an undefined memory location is okay from an equivelance point of view as long as the side effects on the arguments are the same before and after the rewrite.

I think (1) is much safer to uphold in the compiler and I don't have an example why (2) might be useful.

There is also the issue where currently neither the frontend or the rewrites currently uplhold either.

For example, this is an acceptable program by the front-end:

def foo(a: f32 @ DRAM):
    b: f32 @ DRAM
    a = b

stage_mem can propagate undefined values to proc arguments: #527 (comment)

We need anaylsis support for this. @yamaguchi1024 @gilbo can you take a look this to consider it for the analysis revamp?