ICE: Running into "dead code"

[Istvan91]

I managed to hit following "dead code":

// File pats_trans3_env_dvar.dats line 619
          val () = assertloc (false) in s2e // HX: this should be deadcode!

This happened while refactoring and opportunistically trying out some "syntactical shortcut". This is currently the "best" minimal example I managed to come up with:

// reproduction.sats
typedef extBuffer = $extype"union Buffer"
dataview Buffer_v(l:addr, n:int) = buffer_v(l, n) of (extBuffer @ l)
vtypedef Buffer(l:addr) = (Buffer_v(l, 4096) | ptr l)

fn buffer_init
{l:agz}
(!extBuffer? @ l >> Buffer(l)| ptr l): void = "mac#extbuffer_init"

and

// reproduction.dats
staload test = "reproduction.sats"

implement main0() = let
  var buf: $test.extBuffer with pf_buf
  val () = $test.buffer_init(pf_buf | addr@buf)
in
  ()
end

I was not able to reproduce the error when merging the 2 files. When I did so I got a syntax error. It looks like the sats file is parsed differently?

In my original code the solution was to use something like

fn buffer_init
{l:agz}
(!extBuffer? @ l | ptr l): (Buffer(l) | void) = "mac#extbuffer_init"

// instead of
fn buffer_init
{l:agz}
(!extBuffer? @ l >> Buffer(l)| ptr l): void = "mac#extbuffer_init"

Expected Result: Some error message instead of an ICE.

[githwxi]

This was due to Buffer(l) not being an at-view:

fn buffer_init {l:agz} (!extBuffer? @ l >> Buffer(l)| ptr l): void = "mac#extbuffer_init"

Given my understanding, the type for 'buffer_init' should be given as follows:

fun buffer_init {l:agz} (extBuffer? @ l | ptr l): Buffer(l) = "mac#extbuffer_init"

On Wed, May 13, 2020 at 3:10 PM Istvan Ruzman notifications@github.com wrote:

I managed to hit following "dead code":

// File pats_trans3_env_dvar.dats line 619 val () = assertloc (false) in s2e // HX: this should be deadcode!

This happened while refactoring and opportunistically trying out some "syntactical shortcut". This is currently the "best" minimal example I managed to come up with:

// reproduction.satstypedef extBuffer = $extype"union Buffer"dataview Buffer_v(l:addr, n:int) = buffer_v(l, n) of (extBuffer @ l)vtypedef Buffer(l:addr) = (Buffer_v(l, 4096) | ptr l) fn buffer_init {l:agz} (!extBuffer? @ l >> Buffer(l)| ptr l): void = "mac#extbuffer_init"

and

// reproduction.datsstaload test = "reproduction.sats" implement main0() = let var buf: $test.extBuffer with pf_buf val () = $test.buffer_init(pf_buf | addr@buf)in ()end

I was not able to reproduce the error when merging the 2 files. When I did so I got a syntax error. It looks like the sats file is parsed differently?

In my original code the solution was to use something like

fn buffer_init {l:agz} (!extBuffer? @ l | ptr l): (Buffer(l) | void) = "mac#extbuffer_init" // instead offn buffer_init {l:agz} (!extBuffer? @ l >> Buffer(l)| ptr l): void = "mac#extbuffer_init"

Expected Result: Some error message instead of an ICE.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/githwxi/ATS-Postiats/issues/254, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAEXZV32CHCDGND7ESVDMLTRRLWDJANCNFSM4NABIAYA .