spotted compiler assert failure

[Dambaev Alexander]

Hi,

I got assert failure:

```

exit(ATS): [assert] failed: /tmp/ATS-Postiats/src/pats_trans3_env_dvar.dats: 14625(line=619, offs=20) -- 14641(line=619, offs=36)

```

from this code

SATS file:

```

(* abstract viewtype, that describes Bytestring with capacity and size *)
absvt0ype
  Bytestring_vtype
  ( len:int (* size in bytes, which occupied by data *)
  , offset: int (* the offset from base pointer at which data of length len starts *)
  , cap: int (* capacity of the buffer *)
  , ucap: int (* how much unused bytes of buffer available after this bytestring *)
  , refcnt:int (* how many other bytestrings refer to this bytestring *)
  , dynamically_allocated: bool (* if false, then base pointer is statically allocated *)
  , base: addr (* base pointer *)
  ) =
  ( void
  | ( size_t (* len *)
    , size_t (* offset *)
    , size_t (* capacity *)
    , size_t (* available capacity *)
    , size_t (* refcnt *)
    , bool (* is dynamically allocated *)
    , ptr
    )
  )

(* abstract viewtype, that describes Bytestring with capacity and size *)
absvt0ype
  Bytestring_vtype
  ( len:int (* size in bytes, which occupied by data *)
  , offset: int (* the offset from base pointer at which data of length len starts *)
  , cap: int (* capacity of the buffer *)
  , ucap: int (* how much unused bytes of buffer available after this bytestring *)
  , refcnt:int (* how many other bytestrings refer to this bytestring *)
  , dynamically_allocated: bool (* if false, then base pointer is statically allocated *)
  , base: addr (* base pointer *)
  ) =
  ( void
  | ( size_t (* len *)
    , size_t (* offset *)
    , size_t (* capacity *)
    , size_t (* available capacity *)
    , size_t (* refcnt *)
    , bool (* is dynamically allocated *)
    , ptr
    )
  )

vtypedef
  Bytestring(len) =
  {len: nat}[offset,cap,ucap,refcnt:nat][dynamically_allocated:bool][l:agz]
  Bytestring_vtype( len, offset, cap, ucap, refcnt, dynamically_allocated,l)

absview
  Bytestring_v(a:t0ype, len:int, offset:int, cap: int, ucap: int, refcnt:int, dynamically_allocated:bool, l:addr)

(* non-empty bytestring *)
vtypedef
  Bytestring1 =
  [len: pos][offset,cap,ucap,refcnt:nat][dynamically_allocated:bool][l:agz]
  Bytestring_vtype( len, offset, cap, ucap, refcnt, dynamically_allocated,l)

fn
  pack_chars_static
  {n:nat}{l:agz}{a:t0ype}
  ( !array_v( a, l, n) >> Bytestring_v(a, n, 0, n, 0, 0, false, l)
  | i: ptr l
  , sz: size_t n
  ):
  Bytestring_vtype( n, 0, n, 0, 0, false, l)

overload pack with pack_chars_static

```

DATS file:
```

#include "share/atspre_staload.hats"

#define ATS_DYNLOADFLAG 0
 
staload BS="SATS/bytestring.sats"
staload "DATS/bytestring_flat.dats"

implement pack_chars_static{n}{l}{a}(pf | p, sz) =
let
  extern castfn
    believeme
    {n,offset,cap,ucap,refcnt:nat}{dynamic:bool}{l:agz}
    ( !array_v( a, l, cap) >> Bytestring_v(a, n, offset, cap, ucap, refcnt, dynamic, l)
    | ( size_t(n)
      , size_t(offset)
      , size_t(cap)
      , size_t(ucap)
      , size_t(refcnt)
      , bool(dynamic)
      , ptr(l)
      )
    ):<>
    Bytestring_vtype(n, offset, cap, ucap, refcnt, dynamic, l)
in
  believeme( pf | (sz, i2sz 0, sz, i2sz 0, i2sz 0, false, p))
end

fn
  test(): $BS.Bytestring1 = bs where {
  var buf with buf_pf = @[char]('h', 'e','l','l','o')
  prval _ = $showtype buf_pf
  val bs = $BS.pack ( buf_pf | addr@buf, i2sz 5)
}

implement main0() = {
  val s = test()
  val () = assertloc( $BS.isnot_shared s)
  val () = $BS.free s
}

```

I expected, that there will be typechecking error, saying, that  buf_pf is being preserved with wrong type, forcing me to restore it, but instead I got error above.

Is it better to add such issues to git instead of posting here? (just looks like this group is much more alive, than issue tracker on git)

[Hongwei Xi]

>>I expected, that there will be typechecking error, saying, that  buf_pf is being preserved with wrong type, forcing me to restore it, but instead I got error above.

I have seen this issue before.

Basically. for each stack-allocated variable ('buf' in this case), there should be a proof of

some at-view associated with the variable at the end of its life. In this case, the proof associated

with 'buf' is turned into a proof of the view Bytestring_v, which is not an at-view (of the form T@l).

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KwOjyn3i5Md9ZjSk%3D-NexnKdVS1HcM2poPwcgOHx_BUPA%40mail.gmail.com.

[Hongwei Xi]

I just modified the code base to issue an error message in this case

(instead of just reporting a line number of with a compiler crash).

[Dambaev Alexander]

thanks!

This explanation seems reasonable to me

пн, 28 сент. 2020 г. в 12:00, Hongwei Xi <gmh...@gmail.com>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLr8x%3DmsejtkmAYZaJ610CRXnC0B5e-qB2JGoKxHnWOeDg%40mail.gmail.com.